This chapter discusses a computational logic for applicative common Lisp (ACL2), which is both a logic, and a theorem prover for that logic. The system can be more generally considered to be in the group of so-called “proof-checkers” and “proof-assistants."

Proof checking is the automated verification of mathematical theories by a formalization of their primitive notions; once a theory is formalized, a small program, the proof-checker, verifies its correctness. In order to make the formalization process feasible, an interactive proof-development system is needed. A proof assistant is the combination of a proof-development system and a proof checker.

The chapter is structured into three main parts. The first presents a nice introduction to the need for formal methods in computer science, particularly in the design and verification of microprocessors, and includes a brief sketch of the logic and the theorem prover parts of ACL2. The second part covers the paper’s main topic: the demonstration of ACL2 as a mechanized theory of computation. Through several examples of list processing, taken from McCarthy [1], the reader is guided in how to interact with ACL2 in order to obtain some proofs. Especially interesting is the incursion into the modeling of microprocessors; with this goal in mind, a formal model for a toy version of the Java Virtual Machine is presented, and some theorems are proved. The final part lists a number of industrial applications for which ACL2 was used in the late-1990s.

The paper presents no new results, but provides a nice introduction to formal methods in computer science. It includes some interesting examples of how much one can expect from the generalized use of formal methods, in areas as practical as the development, design, and verification of microprocessors.