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,will probably take several months to become an effective ACL2 user.
* 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,