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.