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 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.
* ACL2 as a mathematical logic, and
* be able to construct a proof (in interaction with ACL2).