Methodology to formalize and theoretically validate compiler behavior

[countvajhula]

E.g. wrt. termination of passes. Define a reference compiler and optimizing compiler. Elaborate the sequence of compilation for an input expression in the reference compiler vs the optimizing compiler.

Related: #159

See Validly Verifying that We're Compiling Correctly