Abstract

Compiler verification is an area that has grown considerably in the last 20 years and a newcomer or outsider might mistakenly think that the area is quite crowded. In this talk, I will argue that the state of the art in compiler verification is still quite far from where it ought to be—there is still plenty to do!

This talk will be given from the perspective of the CakeML project, which has developed an end-to-end verified compiler for an ML-like programming language and is perhaps best known as the first formally verified compiler to be bootstrapped inside the logic of a proof assistant.

The focus will be on the research questions: both questions the CakeML project has tackled and yet-to-be-satisfactorily addressed questions that have emerged when attempting to make verified compilers as realistic and far reaching as possible. The questions will revolve around work on top of verified memory management and ruling out unwanted out-of-memory errors, using verified compilers in verified applications and verified stacks, making (components of) verified compilers more reusable, exploring paths to wider use of verified compilers, etc.

My intention is to provide ideas where the current state of the art in compiler verification leaves room for exciting new work.