Gilles Dowek, explorateur des méthodes formelles

Créer un Esperanto pour les systèmes de vérification de preuve (ou assistants de preuve), qui permettent, à l'instar de l'assistant Coq développé par Inria, de vérifier par ordinateur des preuves ou des démonstrations mathématiques : c'est le challenge que poursuit Gilles Dowek, responsable de l'équipe-projet Deducteam du Centre Inria de Saclay et professeur attaché à l'ENS Paris-Saclay. Le logiciel Coq – à la conception duquel il a brièvement contribué au début de sa carrière – est l'un des systèmes de vérification de preuve reconnus en France par l'ANSSI (Agence nationale de la sécurité des systèmes d'information). Cet outil permet de démontrer rigoureusement qu'un produit vérifie bien une certaine propriété, par exemple qu'il n'est pas vulnérable à un certain type d'attaque informatique.

Âgé de 56 ans, Gilles Dowek a consacré une grande partie de sa carrière à ces méthodes formelles.  Féru de philosophie, ce polytechnicien est aussi lauréat du Grand prix de philosophie 2007 de l'Académie française pour son ouvrage Les métamorphoses du calcul, une étonnante histoire des mathématiques (éditions Le Pommier). « Ma première ambition est d'ordre philosophique : il s'agit de proposer une définition de la notion de démonstration mathématique – l'un des rares invariants anthropologiques – utilisable dans tous les pays et avec tous les systèmes », souligne-t-il. Un parcours exemplaire salué aujourd’hui par le Grand prix Inria – Académie des sciences. « J'ai beaucoup de respect pour ce prix qui jouit d'une grande aura et contribue à valoriser les découvertes scientifiques dans la société au sens large », réagit l’intéressé.

Au cœur de sa réflexion : les enjeux de partage posés par la multiplicité des systèmes de vérification de preuve utilisés à travers le monde. « Lors du développement de Coq, au début de ma carrière, j'ai été amené à me poser des questions sur la diversité des langages créés pour Coq et pour les autres systèmes comparables, comme Isabelle (développé en Allemagne), HOL Light (au Royaume-Uni), PVS et Lean (aux États-Unis) ou Mizar (en Pologne), explique le chercheur. Une vingtaine de langages de preuve sont employés actuellement, ce qui pose de mon point de vue des enjeux d'universalité et de partage. La notion de vérité mathématique est un universel anthropologique, que nous devons essayer de préserver, en veillant à ce que les preuves effectuées puissent être lues partout. »

Pour relever ces défis, Gilles Dowek et les chercheurs de Deducteam ont analysé la construction et les fondements théoriques des différents langages de preuve utilisés actuellement (une forme de lambda-calcul dans le cas de Coq). « Nous avons développé un nouveau cadre logique, dénommé Dedukti (ce qui signifie "déduire" en Esperanto) qui permet d'exprimer des théories et des logiques communes pour les différents systèmes, indique le chercheur. Nous traduisons en Dedukti les principales fonctionnalités de chaque assistant de preuve. » Un procédé aux applications très concrètes : l'équipe traduit par exemple en Dedukti le système de méthode formelle TLA+, très utilisé dans le monde industriel, et la méthode B, notamment employée par la RATP pour vérifier la correction des logiciels embarqués sur plusieurs lignes de métro automatisées.

Pour le chercheur, ce travail est source de grandes satisfactions et d’instants parfois inoubliables, tant au niveau collectif qu'individuel. Un exemple :

L'une de mes plus grandes joies est liée à un article que j'ai écrit presque en une nuit, en août 2006. Cet article, fondateur pour Dedukti, était un moment de grâce : je suis resté bloqué pendant des semaines, puis j'ai eu une idée toute simple, et ma démonstration s'est mise à fonctionner de façon très fluide.

La prochaine étape ? Faciliter la traduction des preuves générées par chaque système et leur partage avec des dispositifs composites comme B ou TLA+ qui utilisent différents « prouveurs externes » pour effectuer leurs vérifications. « Les traductions facilitent et accélèrent les échanges de preuves de sûreté et de sécurité. Elles sont réclamées par les autorités nationales de sécurité des systèmes d'information », détaille Gilles Dowek. Deux exemples : « En France, l'ANSSI demande des preuves effectuées en Coq ou en B, tandis que son équivalent allemand, le BSI (Bundesamt für Sicherheit in der Informationstechnik), privilégie les preuves effectuées en Isabelle. »

Signe du potentiel de Dedukti, ce cadre logique est désormais utilisé par un nombre croissant d'utilisateurs internationaux, notamment au Japon, au Brésil, en Israël et aux États-Unis. Une belle consécration pour Gilles Dowek et ses collègues de l’équipe-projet Deducteam.