Suppose the machine being modeled is some kind of arithmetic unit. Suppose
the model can be initialized so as to **multiply** **x** times **y** and
leave the answer in **z**. Then if we initialize **s** to **multiply** with
**x=5** and **y=7** and run the machine long enough, we can read the answer
**35** in the final state.

Because ACL2 is a programming language, our model can be **run** or
**executed**.

If you defined the model in ACL2 and then typed

(lookup 'z (mc (s 'mult 5 7) 29))

then ACL2 would compute 35. (Here we assume that the function `s`

creates
a state ready to run a given application on given inputs `x`

and `y`

.)
You can **emulate** or **test** the model of your machine.

This is **obvious** because ACL2 is Common Lisp; and Common Lisp is a
**programming language**.