A Formally-Verified Lisp, or

Explorations in the Formal Verification of McCarthy's Equations

While reading through CPDT, it occurred to me that figuring out a project that I could work which also included formal verification would be immensely useful in cementing what I was learning. Awash in a sea of Theorems, →s, Inductions, and ∀ xs, it somehow occurred to me that implementing a Lisp would be illuminating (probably sparked by watching Jeremy starting to work through "Build Your Own Lisp").

Fundamentally, if Lisp can be expressed as a set of equations, then it is conceivable that it could be defined using formal methods, allowing for a more rigorous examination of the properties of the resulting system. This is made more difficult by the fact that I never made it very far in school, therefore both my computer science and mathematical backgrounds are lacking; in a way, this one of the efforts that I think will bring me a better understanding of the theory behind computing in practical manner better suited to how I learn.

I'm putting the code (and a tentative, in-progress paper that I'm writing on the subject) on Github, and the draft version of something like a paper (written in Markdown) is also around. The paper will probably be updated most rapidly, but I am attempting to keep the Markdown version relatively in-sync.