Research
In general, I am interested in using techniques from
programming language theory and formal methods to improve our
experience of the digital world. I start from this simple
observation: using a computer in 2024 is a dreadful experience.
The average user is more likely to equate computers with
crashes, freezes, overall slowness and unresponsiveness, and
bugs in general, rather than see computers as helpful tools
that improve their life. On top of that, our increasing
dependence on computer systems can only frustrate users who now
have to use buggy systems to manage every part of their life.
Worse, because such a large part of our digital life is managed
by unreliable systems, we live at the mercy of the next
devastating bug such as Heartbleed or
the
CrowdStrike outages; and the best we can do is hope that
the next bug will be patched quick enough.
Yet, this doesn't have to be the case! In the last few
decades, a lot of progress has been made in terms of verifying
programs: researchers have built verified compilers, kernels, cryptographic libraries,
etc. Model checking tools such as TLA+ have
been used successfully to model and verify the properties of
real-life systems used in industry. At the same time, safer and
saner languages such as Rust have become increasingly
popular, as they allow writing safe programs without
compromising on performance.
I am hoping that, in the future, we'll be able to combine
all these techniques, as well as other ones such as worst-case
execution time analysis, to make using computers safer, easier,
and less frustrating. As a strong believer in formal methods, I
believe that in a few decades at most, we'll be able to
convince even the most reluctant developer of their benefits.
In the meantime, I aim to improve the formal methods ecosystem,
and show that they can be used to build reliable computer
systems.
