The Marriage of Effects and Proof Assistants – ProverFX

Formal software correctness is gaining traction, with a paroxysmal application to lethal issues in medicine and autonomous vehicles. Interactive theorem provers based on type theory have shown their effectiveness to prove correctness of important pieces of software like the toolchain of the DeepSpec project. However, they suffer from a major limitation: the absence of effects. This means from a programming point of view that all certified programs are pure, e.g., without exceptions or mutable states, leading to efficiency issues of the extracted code. This also means from a logical point of view that we do not have access neither to classical reasoning nor to the axiom of choice, leading to expressivity issues of the logic. Putting aside efficiency and expressivity, adding effects would enable to go beyond the “all programs and proofs must be fully specified and terminating” paradigm, which prevents developers from quick prototyping and testing before entering the full certification process. But the reason for this limitation is quite strong and known from the 90’s: naively adding effects gives rise to logically inconsistent proof assistants.

Recently, the PI’s group has opened a breach through which effects can be integrated into proof assistants by taming the power of dependent types using a generalization of Grothendieck universes. Based on this radically new approach, the ProverFX project will provide a family of proof assistants where computational and logical effects can be added to the initial theory using compilation phases, without corrupting the logic. These compilation phases will themselves be certified inside a proof assistant— which, together with the certification of the original system, allows to move from a trusted code base to a trusted theory base paradigm. Those extensions will considerably increase the kind of software systems that can be certified by non-expert engineers, as well as the kind of proofs mathematicians will be able to formalize.