How Long Does It Take to Become an Effective User?

The training time depends primarily on the background of the user.

We expect that a user who

  * has a bachelor's degree in computer science or mathematics,

* has some experience with formal methods,

* has had some exposure to Lisp programming and is comfortable with the Lisp notation,

* is familiar with and has unlimited access to a Common Lisp host processor, operating system, and text editor (we use Sun workstations running Unix and GNU Emacs),

* is willing to read and study the ACL2 documentation, and

* is given the opportunity to start with ``toy'' projects before being expected to tackle the company's Grand Challenge,

will probably take several months to become an effective ACL2 user.