Building trustworthy software with CakeML

CakeML is an impure functional programming language aimed at supporting formally verified programs. The CakeML project has several aspects including formal semantics and metatheory, a verified compiler, a mechanised connection between its semantics and higher-order logic (in the HOL4 interactive theorem prover), and an example verified theorem prover written in CakeML and HOL4. It also has respectable performance compared to industrial-strength implementations of ML. The CakeML project has been running for six years and has achieved its initial goal of demonstrating the feasibility of a practical, mechanically verified compiler from program source text to target machine code. But where should we go from here? In this talk, I will present an overview of the compiler, and the techniques we used to verify it. I will also present some example applications which have been built atop CakeML, and speculate on the role that a verified compiler can play in building trustworthy software.