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.
