Relation to Common Lisp, including deviations from the spec
ACL2 is a logic, a theorem prover, and a programming language based on Common Lisp. A connection with Common Lisp is established with guards (see guard).
However, here we document potential deviations from Common Lisp semantics even in the presence of verified guards. Our view is that these deviations are extremely unlikely to manifest; indeed, as of this writing we are unaware of any cases in which these issues arise in practice. However, we feel obligated to acknowledge their possibility, which could result in surprises during evaluation or even proof.
The Common Lisp spec allows certain predicates to return what it calls
``generalized Booleans,'' which are really arbitrary values that are to be
viewed as either
The execution of forms with
The Common Lisp spec, specifically
Section Section 220.127.116.11
of the Common Lisp Hyperspec,
allows for undefined results when a function is ``multiply defined'' in a
compiled file. ACL2 allows redundant defuns in a book, and in general
books are compiled by