ACL2: an industrial strength version of Nqthm

Abstract

ACL2 ("A Computational Logic for Applicative Common Lisp") is a reimplemented extended version of Boyer and Moore's (1979, 1988) Nqthm and Kaufmann's (1988, 1990, 1992) Pc-Nqthm, intended for large-scale verification projects. However, the logic supported by ACL2 is compatible with the applicative subset of Common Lisp. The decision to use an "industrial strength" programming language as the foundation of the mathematical logic is crucial to our advocacy of ACL2 in the application of formal methods to large systems. However, one of the key reasons Nqthm has been so successful, we believe, is its insistence that functions be total. Common Lisp functions are not total and this is one of the reasons Common Lisp is so efficient. This paper explains how we scaled up Nqthm's logic to Common Lisp, preserving the use of total functions within the logic but achieving Common Lisp execution speeds.