• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • Common-lisp
          • Defun-mode-caveat
          • Generalized-booleans
          • Raw-lisp-error
          • Escape-to-common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• About-ACL2

Common-lisp

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 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 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.

Subtopics

Defun-mode-caveat

Potential soundness issue for functions with defun-mode :program

Generalized-booleans

Potential soundness issues related to ACL2 predicates

Raw-lisp-error

Raw lisp errors

Escape-to-common-lisp

Escaping to Common Lisp