TRIMabstract machine, and an algebraic framework was used for the correctness proof, based on equational specifications for the syntax and semantics of both the source and target languages. Correctness is proved by showing that the source semantics is preserved by the translation (compilation) into the target semantics. The compiler was implemented in C++ and actually produces quite efficient code.
The style of this example is rather informal, in that complete logical rigor was neither attempted nor achieved. In particular, some of the lemmas only have intuitive explanations, not formal proofs. We view this as an advantage for the purpose of illustrating our approach, because it shows that we can support industrial style proofs, where it is not regarded as economically worthwhile to achieve full formality.