We expect that a talented undergraduate majoring in computer science (or perhaps mathematics) will probably take several weeks to become an effective ACL2 user. The time will depend, of course, on that student's familiarity with logic (or formal methods) and Lisp programming, as well as willingness to read and study the ACL2 User's Manual.
Of course, it is critical to do some projects in order to gain proficiency. (Hence access to an ACL2 implementation is also a requirement, for example by downloading and installing following links from the ACL2 home page.) But it is critical to start with ``toy'' projects before tackling a ``grand challenge.''
