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.
