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,