ACL2 is used to construct mathematical models of computer hardware and software (i.e., ``digital systems'').

A **mathematical model** is a set of mathematical formulas used to predict
the behavior of some artifact.

The use of mathematical models allows **faster** and **cheaper** delivery of
**better** systems.

Models need not be **complete** or **perfectly accurate** to be useful to the
trained engineer.

Click here for more discussion of these assertions in an engineering context.