Major Section: MISCELLANEOUS
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.
:program
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 nil or non-nil. However, in ACL2 these functions
are assumed to return nil or t. For
details,see generalized-booleans.
The execution of forms with :program mode functions can result in
calls of functions on arguments that do not satisfy their guards. In
practice, this simply causes hard Lisp errors. But in principle one could
imagine a damaged Lisp image that operates incorrectly.
See defun-mode-caveat.
The Common Lisp spec, specifically Section 3.2.2.3 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 certify-book (but
see certify-book and see compilation for how to control such compilation).
Moreover, ACL2 provides a redefinition capability
(see ld-redefinition-action and see redef), and the above section also
allows for undefined results when a function is defined in a compiled file
and then redefined, presumably (for example) because of inlining.
