Background

Alan Kay once described a certain half-page of code in the Lisp 1.5 manual as the "Maxwell's Equations of Software", noting

This is the whole world of programming in a few lines that I can put my hand over.

What are these equations?

If we posit that these equations are, in fact, an analogue of Maxwell's equations that capture a description of "the whole world of programming" in a mathematically precise language, can a formally-verified implementation be built? What does this implementation tell us about the world of programming?

Some core questions this might immediately invoke are,

• What is the syntax of a formally-verified Lisp?
• What are the semantics of a formally-verified Lisp?
• What guarantees can we make about the behaviour of VLisp?
• Working under the assumption that Lisp (in particular, a Lisp derived from the equations in Figure 1) can be considered as a sort of ``McCarthy's Equations of Software'' (MEoS), what theorems can be made regarding its behaviour and properties?
• What are the practical, useful implications of these theorems?

While the end goal is to build a formal model of Lisp from McCarthy's equations, it will be necessary to implement the first chapter of the Lisp 1.5 manual, "The Lisp Language".

The Lisp Language

Before delving into a software implementation, let us consider Lisp, the language.

McCarthy splits the language into two notations:

• S-expressions (symbolic expressions) are the notation of Lisp programs,

• M-expressions (meta-expressions) are the notation of the source language that specifies how to process S-expressions.