# what1fool.info

## 1 TODO proof that Emacs Lisp is Turing complete

One strategy that seems to be commonly recommended: Prove that your system X is Turing complete by implementing a simple known-to-be-Turing-complete system inside of X.

one article that works through this process

another paper that seems relevant

I haven't done this for elisp yet, obviously.

Ideally I would also like to see a mechanically checked version of this proof, but I don't presently have the skills to do something like that in Coq, Agda, etc.