Editing ACL2 (section)

==Overview==
The ACL2 programming language is an [[applicative programming language|applicative]] ([[Side-effect (computer science)|side-effect]] free) variant of Common Lisp.  ACL2 is untyped. All ACL2 [[Subroutine|functions]] are [[Total function|total]]&nbsp;— that is, every function maps each object in the ACL2 [[Universe (mathematics)|universe]] to another object in its universe.

ACL2's base theory [[axiom]]atizes the [[semantics]] of its programming language and its built-in functions.  User definitions in the programming language that satisfy a ''definitional principle'' extend the theory in a way that maintains the theory's [[Consistency proof|logical consistency]].

The core of ACL2's theorem prover is based on [[term rewriting]], and this core is extensible in that user-discovered [[theorem]]s can be used as ad hoc [[Mathematical proof|proof]] techniques for subsequent [[conjecture]]s.

ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover, [[Nqthm|NQTHM]].  Toward this goal, ACL2 has many features to support clean engineering of interesting mathematical and computational theories.  ACL2 also derives efficiency from being built on Common Lisp; for example, the same specification that is the basis for inductive verification can be [[Compiler|compiled]] and run [[native code|natively]].

In 2005, the authors of the Boyer-Moore family of provers, which includes ACL2, received the [[ACM Software System Award]] "for pioneering and engineering a most effective theorem prover (...) as a formal methods tool for verifying safety-critical hardware and software."<ref>{{Cite web|url=http://campus.acm.org/public/pressroom/press_releases/3_2006/software.cfm|title=ACM: Press Release, March 15, 2006|date=August 1, 2008|archive-url=https://web.archive.org/web/20080801092315/http://campus.acm.org/public/pressroom/press_releases/3_2006/software.cfm |archive-date=2008-08-01 }}</ref><ref name=acmaward>{{cite web|publisher=[[Association for Computing Machinery]] |url=http://awards.acm.org/homepage.cfm?srt=all&awd=149 |work=ACM Awards |title=Software System Award |access-date={{Format date|2012|1|14}} |url-status=dead |archive-url=https://web.archive.org/web/20120402203501/http://awards.acm.org/homepage.cfm?srt=all&awd=149 |archive-date=2012-04-02 }}</ref>