More posts like this, please.
Excellent point! Compiling Lambda Calculus is a bit like this. It starts with Lambda Calculus and then develops multiple implementations of increasing complexity. LISP from Nothing also does this, but it is about ancient LISP.
I will definitely keep this in mind!