The original NQTHM project started back in the 1971, when Moore was a PhD student at the U. of Edinburgh after graduating from MIT, and when he met Boyer. They were influenced by Woody Bledsoe and the insight that proving theorems by resolution was actually programming in predicate calculus.
This insight was fully realized in ACL2 -- which stands for ``A Computational Logic for Applicative Common Lisp'' -- written in a pure-applicative (i.e., pure functional) subset of Common Lisp. The theorem specification and the implementation languages become the same! The prover can therefore prove a part of itself. Furthermore, since the ACL2 specification is the Common Lisp code, it can be compiled and executed. One may not only prove properties of a specification, but also run it directly, as, hence, a provable implementation. That fact turned out quite useful when proving correctness of the AMD Athlon floating point unit.
J. Strother Moore remarked that his experience of writing and maintaining the imperative prover NQTHM for 18+ years, and the similar 11-year experience for the pure-functional ACL2 prover showed the applicative style is better. He said that he will never go back to the imperative style.
<http://www.cs.utexas.edu/users/moore/>
J. Strother Moore home page. See specifically his ``My'' Best Ideas page.
Besides theorem provers, he, together with Boyer, discovered their eponymous string matching and majority voting algorithms, and invented the efficient method of formula (and, general text) editing, which was later employed in MS Word. In his PhD theses J. Strother Moore also developed a Prolog-like language in Lisp, at the same time frame as Prolog itself.
Each proven lemma is automatically added to the database of known true facts -- and can immediately be used in proving other theorems. We can also prove re-writing rules and reasoning strategies -- and add them to the database for later use. The prover becomes smarter with every successful proof.
In the 80s, Boyer, Moore and their students proved undecidability of the halting problem, and the Goedel First incompleteness theorem. The latter proof required 2000 lemmas. They proceeded to prove the design of a sample microprocessor, the correctness of the assembler for a micro-processor, and even the correctness of a simple OS.
<http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/innovations.html>
NQTHM key ideas
<http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/index.html>
The complete list of proved results
The ACL2 prover is 72KLOC long. The documentations takes 1.7 MB; in addition; comments in the code occupy 1.2 MB. Whenever the authors extent or correct a function, they describe the motivation and the action in the comments. Thus ACL2 comments reflect thirty years of the evolution of the theorem provers.
As the ACL2 web page says, ``I think it's really cool that the system is coded in its own logic. How many theorem provers can you say that about? How many 5 Mbyte applicative programs can you name?''
The ACL2 is used quite frequently for real projects (proofs of correctness for the AMD Athlon FPU, for a Motorola DSP processor, for a JVM chip and for a strcpy()/strcat()/... UNIX string library), partly because it is fast. ACL2 has plenty of tricks to speed up proofs, for example, "lazy" beta-reduction. The latter tries to bundle several pending beta-reductions and execute them during a single traversal of a potentially huge term. For example, a correctness proof of a Motorola CAP DSP processor generated an intermediate formula that was 25MB long. ACL2 can deal with even bigger formulas.
<http://www.cs.utexas.edu/users/moore/best-ideas/acl2/index.html>
ACL2 summary and innovations
<http://www.cs.utexas.edu/users/moore/acl2>
ACL2 home page
It lists two books, several ACL2 workshops. The site contains the full, hyperlinked ACL2 documentation. ACL2 is freely downloadable from the above site.
ACL2 !>(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x))
(list (car x)))))
The system responds with
The admission ofREVis trivial, using the relationE0-ORD-<(which is known to be well-founded on the domain recognized byE0-ORDINALP) and the measure(ACL2-COUNT X). We observe that the type ofREVis described by the theorem(OR (CONSP (REV X)) (EQUAL (REV X) NIL)). We used primitive type reasoning and the:type-prescriptionruleBINARY-APPEND.
Note how the system figured out the type of rev. The type is
formulated as a theorem, which can be proved by ACL2 and then used as
a side condition whenever function rev is applied. Curry-Howard
isomorphism in action! For that reason, a static type system is not
necessary.
Still, J. Moore keeps an open mind. When asked what he would do if he started with an empty Emacs buffer now, he replied that he would give Haskell a very hard look. One of his (former) students is playing with Haskell to this end; so far, Moore said, he was able to closely and elegantly emulate in ACL2 all the Haskell code that person sent him. J. Moore is a bit concerned how Haskell will play out in terms of performance. He didn't mention any studies though.
The FP unit was specified in a Register Transfer Language (RTL) -- a common hardware description language that describes registers of various logical/arithmetical components and data transfers. To prove the correctness of FPU, Moore and his group had to develop a translator from RTL to ACL2, the input language of the prover. Moore had to convince the AMD management that the translation is sound. Alas, RTL is not specified precisely; its semantics is defined by an RTL emulator.
The fact that ACL2 specification is itself ACL2 code, which is applicative Common Lisp code, turned out very handy: ACL2 specifications can be executed. The ACL2 specification for the FPU can therefore be considered an emulator for the FPU: it takes bit patterns representing input FP numbers and prints the output bit patterns. To convince the management that the ACL2 FPU specification is a sound representation of the original RTL specification, one needs to show that the two FPU emulators are equivalent. The management gave Moore 80 million test vectors, designed to verify the RTL specs. The compiled ACL2 specs code produced the same results for these vectors as the RTL emulator. That convinced the AMD management that the ACL2 specs accurately reflect the RTL code for their FPU. After that, Moore and his students proceeded to prove that the ACL2 FPU specs are consistent with the IEEE arithmetic rules. They found four real bugs -- which were confirmed as bugs by the RTL emulator. These four bugs survived all previously tried 80 million test vectors!
Moore and his students later proved correctness theorems for an IBM 4758 crypto-processor. The theorems contributed to the crypto-processor's being awarded IFIPS 140-1 rating, the highest security rating for any piece of hardware and software.
<http://www.cs.utexas.edu/users/moore/best-ideas/acl2/index.html>
More (industrially important) results proved by ACL2