## What is Required of the User?

It is not easy to build ACL2 models of complex systems. To do so, the
user must **understand**

* the system being modeled, and
* ACL2, at least as a programming language.

It is not easy to get ACL2 to prove hard theorems. To do so, the user must
**understand**

* the model,
* ACL2 as a mathematical logic, and

* be able to construct a proof (in interaction with ACL2).

ACL2 will help construct the proof but its primary role is to prevent
logical mistakes. The creative burden -- the mathematical insight into
**why the model has the desired property** -- is the user's responsibility.