Dale Miller : faire que la preuve soit universelle

Dale Miller en est convaincu : l’obtention du financement ERC va les aider lui et Parsifal, son équipe-projet, à avancer de façon significative sur le long chemin de la preuve. Et cette avancée bénéficiera à tout le monde ! Cette preuve est un peu le Graal des chercheurs en sciences informatiques et mathématiques. Comment prouver qu’un logiciel ou un circuit électronique font bien ce qui est attendu d'eux et qu’ils le font dans les conditions et conformément aux spécifications qui ont présidé à leur création ? Pour prouver la validité d’un programme de plusieurs millions de lignes de code, il faut parfois concevoir un nouveau programme, composé lui de plusieurs centaines de milliers de lignes de code…

Le sujet est loin d’être trivial. Les systèmes numériques se multiplient et pas seulement dans les domaines des loisirs ou du divertissement, domaines dans lesquels l’utilisateur peut relancer lui-même son système en cas d’erreur ou se passer d’une fonction si elle est affectée par un bug. Aujourd’hui, des codes et des programmes pilotent, contrôlent, automatisent de nombreuses tâches qui ont un impact sur nos vies quotidiennes et qui ne tolèrent aucun dysfonctionnement. Le lancement d’une fusée  qui va larguer un satellite de communications supposé fonctionner de façon autonome pendant une quinzaine d’années doit être fiabilisé à 100%. De même, le monitoring de la température d’une couveuse ou du rythme cardiaque d’un patient qui vient d’être opéré du cœur ne supporte aucune défaillance. Sans parler des avions de ligne, des systèmes de transactions bancaires, des télécommunications, etc. À cela s’ajoute la question de la sécurité, c’est-à-dire comment protéger tous ces objets numériques des virus et des attaques malveillantes.

Dale Miller travaille sur ces sujets depuis longtemps. Après un Ph.D. en mathématiques à l’université de Carnegie Mellon, il est professeur et chercheur en informatique. D’abord aux États-Unis, puis en Europe où sa matière, la logique computationnelle, bénéficie d’un grand intérêt des milieux de la recherche. Edimbourg, Glasgow, Gênes, Pise, Sienne l’attirent tout particulièrement. Mais c’est en France qu’il trouve son centre de gravité. Cet Américain marié à une Italienne, s’installe en région parisienne en 2002 lorsqu’il devient directeur de recherche au centre Inria de Saclay et professeur à l’École polytechnique. Son français, selon lui, n’est pas à la hauteur de son investissement dans la recherche hexagonale, « il faudrait que je quitte le labo si je voulais vraiment parler français !  », affirme-t-il. C’est vrai qu’il est quotidiennement entouré d'une équipe cosmopolite : un Allemand, un Américain, un Indonésien, des Néerlandais, des Italiens... et quelques Français. Et que la langue de travail dans la recherche reste l’anglais !

L’idée est de créer une place de marché où il sera possible d’échanger et de partager les systèmes de preuve élaborés ici ou là.

Il invoque la Tour de Babel, non pour parler du multilinguisme de son environnement, mais bien pour décrire la situation en matière de preuve. « Il n’existe aucun standard dans ce domaine. Chaque fois qu’il faut prouver qu’un système fonctionne, il faut un budget et un étudiant pour développer un vérificateur des preuves de propriétés du système. Et encore, ce vérificateur est conçu ad hoc et il ne fonctionne que pour un seul système. Parfois, il ne marche même pas pour la version suivante du système ! » Le contre-exemple le plus explicite est celui des fichiers texte : « depuis que quelqu’un a inventé le langage html, les fichiers peuvent être lus par n’importe quel navigateur. C’est ce à quoi nous voulons parvenir dans le domaine de la preuve. »

Son idée : faire de la « chimie informatique », c’est-à-dire utiliser les atomes d’inférences existants pour élaborer des molécules d’inférences. Autrement dit, proposer des modules de systèmes de preuves certifiés pour pouvoir composer un système arbitraire… « L’idée est de créer une place de marché où il sera possible d’échanger et de partager les systèmes de preuve élaborés ici ou là. » Pour parvenir à cela, Dale Miller envisage de délivrer des "certificats de preuve", c’est l’objet du projet ProofCert qui lui a valu la bourse ERC. « En fait, ce sujet est très abstrait, mais il a un vrai impact sur le monde réel et sur notre vie...  », conclut-il.