As software invades every single aspect of our daily lives, the consequences of poorly written, insecure code become more and more drastic. An unreliable phone, or a crashy desktop app are bothersome but may cause no harm; an incorrect algorithm has dramatic consequences, resulting in a loss of privacy, security, money or even lives.

My research focuses on designing tools and methodologies that can make trustworthy software a reality, using formal methods. In particular, this involves a close collaboration with existing software practicioners, to make sure that the fruits of our research are in a form that is usable now.

Project Everest is about putting these principles in practice. Using the Low* toolchain (ICFP’17), we compile a subset of F* (POPL’17) programs to C code. Via a series of paper proofs, we show that the compilation from Low* to C preserves semantics. As a result, libraries like HACL* (CCS’17) generate verified C code that can be integrated within existing software such as Firefox.

BBC micro:bit (2014-2016)

Just like arithmetic or reading, basic computer skills are now indispensable to navigate the modern world. The BBC micro:bit is a micro-controller that was handed out for free to all 7th-graders in the UK. Along with an accessible user interface and programming model, this board effectively made computer science education free and for all. I worked on core components of the programming interface (ICSE’16), in close collaboration with ARM and University of Lancaster.

The micro:bit is now managed by a foundation, is available worldwide, and has been shown to have a lasting impact on British society.

Mezzo (2010-2014)

A first foray into designing more reliable programming languages, Mezzo brought together the ML programming model and separation logic using a notion of permissions. Equipped with a powerful dependent type system (TOPLAS’15), Mezzo gave the programmer the ability to reason about ownership, hence ruling entire classes of bugs such as data races (ICFP’13). Mezzo was mechanically formalized (FLOPS’14) and is available to play with online.