## Common Lisp as a Modeling Language

In ACL2 we have adopted Common Lisp as the basis of our modeling language.
If you have already read our brief note on Common Lisp and recall the example
of `app`

, please proceed. Otherwise click here for an
exceedingly brief introduction to Common Lisp and then come **back** here.

In Common Lisp it is very easy to write systems of formulas that manipulate
discrete, inductively constructed data objects. In building a model you
might need to formalize the notion of sequences and define such operations as
concatenation, length, whether one is a permutation of the other, etc. It is
easy to do this in Common Lisp. Furthermore, if you have a Common Lisp
``theory of sequences'' you can **run** the operations and relations you
define. That is, you can execute the functions on concrete data to see what
results your formulas produce.

If you define the function `app`

as shown above and then type

(app '(A B) '(C D E))

in any Common Lisp, the answer will be computed and will be
`(A B C D E)`

.
The **executable** nature of Common Lisp and thus of ACL2 is very handy when
producing models.

But executability is not enough for a modeling language because the purpose
of models is to permit analysis.

Click here to continue.