ACL2s: "The ACL2 Sedan"
Peter C. Dillinger, Panagiotis Manolios, J S. Moore, and Daron Vroon.
User Interfaces for Theorem Provers Workshop, 2006. © Elsevier
ACL2 is the latest inception of the Boyer-Moore theorem prover,
the 2005 recipient of the ACM Software System Award. In the hands
of experts it feels like a finely tuned race car, and it has been
used to prove some of the most complex theorems ever proved about
commercially designed systems. Unfortunately, ACL2 has a steep
learning curve. Thus, novices tend have a very different
experience: they crash and burn. As part of a project to make
ACL2 and formal reasoning safe for the masses, we have developed
ACL2s, the ACL2 sedan. ACL2s includes many features for
streamlining the learning process that are not found in ACL2. In
general, the goal is to develop a tool that is "self-teaching,"
i.e., it should be possible for an undergraduate to sit down and
play with it and learn how to program in ACL2 and how to reason
about the programs she writes.
PDF (325K) © Elsevier