The next 700 verified compilers

Software can be proved (i.e. verified) to function correctly.

However, many verification efforts leave a gap between the source code that is proved correct and the executable machine code that actually runs.

This gap can be bridged using verified compilers, since verified compilers ensure that correctness properties proved of the source code also hold for the executable machine code.Even though there is a plethora of programming languages, there are currently only two verified end-to-end compilers with decent performance: CompCert for the C language and CakeML for a SML-style language.

These two compilers have taken many years to develop, and currently it is overly difficult to build new verified compilers for new languages, even from the two that exist.The work described here will (1) produce three new reusable compiler building blocks and (2) demonstrate that these can — with ease — be used to build new end-to-end verified compilers and language implementation for a range of languages, including languages in the style of SPARK/Ada, Python, Haskell and JavaScript, which will be implemented using just-in-time compilation.The CakeML compiler will be used as the starting point for this four-year project, which will see me working at 25 % for four years and a postdoc at 100 % for two years.The most challenging aspect of this work will be the design of a clean way of including the compiler itself in the generated code in the context of verified just-in-time compilation.