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.
