Gilles Dowek: an explorer of formal methods

Gilles Dowek, head of the Deducteam project team at the Inria Saclay Centre and guest professor at ENS Paris-Saclay, is seeking to create an Esperanto for proof verification systems (also known as proof assistants) which, like the Coq assistant developed by Inria, are used to verify mathematical proofs. Coq – which Dowek made a brief contribution to early on in his career – is one of the proof verification systems to have been recognised by the ANSSI (the French cybersecurity agency). It is used to rigorously demonstrate that a product verifies a certain property, e.g. that it is not vulnerable to a certain type of cyberattack.

Now 56, Gilles Dowek has spent a large chunk of his career on these formal methods.  A devotee of philosophy, this graduate of the École Polytechnique was previously awarded the Philosophy Grand Prize by the Académie Française in 2007 for his book Les métamorphoses du calcul, une étonnante histoire des mathématiques (published by Le Pommier). “My primary ambition is philosophical: to come up with a definition for the concept of a mathematical proof - a rare anthropological invariant - that can be used in all countries and with all systems.” In recognition of his remarkable career, Gilles Dowek has been awarded the Inria - French Academy of Sciences Grand Prize. “I have a great deal of respect for this award, which carries a lot of weight and helps to promote scientific discoveries within the wider society.”

One of the challenges Gilles Dowek is seeking to address is the vast array of different proof verification systems used across the world. “When working on the development of Coq early on in my career, I found myself thinking about the wide range of languages created for Coq and other comparable systems, such as Isabelle (developed in Germany), HOL Light (developed in the UK), PVS and Lean (developed in the USA) or Mizar (developed in Poland). Around twenty or so proof languages are currently in use, which creates issues with regard to universality and sharing. The concept of mathematical truth is an anthropological universal that we must strive to preserve, making sure that proofs can be read everywhere.” 

In response to these challenges, Gilles Dowek and the researchers from Deducteam analysed the construction and the theoretical foundations of different proof languages currently in use (a form of lambda calculus for Coq). “We developed a new logical framework, Dedukti (which means "to deduce” in Esperanto), for expressing common logics and theories for different systems. The main features of each proof assistant are translated into Dedukti.” This process has some highly practical applications: the team has translated both the formal specification language TLA+, which is widely used in industry, and the B method, which is used by the RATP (the public transport operator in Paris) to verify any corrections made to the software used on a number of automated metro lines.

This work has been extremely rewarding for Gilles Dowek, providing him with some unforgettable moments at both a collective and a personal level.

One of my happiest memories goes back to an article I wrote pretty much in one night back in August 2006. That article was crucial to the development of Dedukti, and it was like everything just came together: I had been stuck for weeks, then I came up with this very simple idea and my proof started to work really smoothly.

The next step will be to make it easier to translate proofs generated by individual systems and share them with composite systems such as B or TLA+, which use different “external provers” for verification. “Translations make sharing safety and security proofs easier and quicker, and are demanded by national cybersecurity agencies.  In France, the ANSSI requires proofs to be in either Coq or B, while its German equivalent, the BSI (Bundesamt für Sicherheit in der Informationstechnik) prefers proofs in Isabelle.” 

Dedukti is now being used by a growing number of international users, in countries such as Japan, Brazil, Israel and the USA, underlining the potential of this logical framework. This is also testament to all of the hard work put in by Gilles Dowek and his colleagues from Deducteam.