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.