It is very difficult at present to verify implementations written in industry standard high-level programming languages such as C and Java because these languages are too complex to have tractable formal definitions, making it impossible to rigorously prove properties about designs expressed in them. As a partial solution, we can program some practically useful systems directly in logic, and then compile the logic to realistic platforms for execution.

We specify applications such as cryptographic algorithms and the mathematics needed for their verification in the higher order logic of the HOL theorem prover, and then deductively compile the specifications to low level code. The correctness of the compilation is proved automatically, producing theorems which guarantee the equivalence of the transformed code and the original specifications. In this talk, we discuss how such a compiler is constructed and verified. This compiler relies heavily on term rewriting to perform program transformations. Moreover, we present how to specify a wide spectrum of compiler optimizations in temporal logic (e.g. Regular CTL).