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.
