Un nouvel « Entretien autour de l’informatique ». Gilles Dowek est chercheur en informatique chez Inria et enseignant à l’ENS de Paris-Saclay. Il est 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 de mathématiques (éditions Le Pommier) et du Grand prix Inria – Académie des sciences 2023 pour ses travaux sur les systèmes de vérification automatique de démonstrations mathématiques. Il a brièvement travaillé sur le système Coq au début de sa carrière. Il est à l’origine de Dedukti, un cadre logique permettant d’exprimer les théories utilisées dans différents systèmes de vérification de démonstrations. C’est l’une des personnes qui a le plus contribué à l’introduction en France de l’enseignement de l’informatique au collège et au lycée.
Binaire : Comment doit-on te présenter ? Mathématicien, logicien, informaticien ou philosophe ?
GD : Le seul métier que j’aie jamais exercé, c’est informaticien. La séparation des connaissances en disciplines est bien sûr toujours un peu arbitraire. Il y a des frontières qu’on passe facilement. Mes travaux empiètent donc sur les mathématiques, la logique et la philosophie. Mais je suis informaticien.
Binaire : Peux-tu nous raconter brièvement ta vie professionnelle ?
GD : Enfant, je voulais déjà être chercheur, mais je ne savais pas dans quelle discipline. Les chercheurs que je connaissais étaient surtout des physiciens : Einstein, Marie Curie… Je voyais dans la recherche une construction collective qui durait toute l’histoire de l’humanité. J’étais attiré par l’idée d’apporter une contribution, peut-être modeste, à cette grande aventure. Mes fréquentes visites au Palais de la Découverte m’ont encouragé dans cette voie.
J’ai commencé ma carrière de chercheur assez jeune grâce à l’entreprise Philips, qui organisait, à l’époque, chaque année un concours pour les chercheurs de moins de 21 ans, des amateurs donc. J’ai proposé un programme pour jouer au Master Mind et j’ai obtenu le 3ème prix. Jacques-Louis Lions qui participait au jury a fait lire mon mémoire à Gérard Huet, qui l’a fait lire à François Fages. J’avais chez moi en 1982 un ordinateur avec 1 k-octet de mémoire et mon algorithme avait besoin de plus. Je ne pouvais l’utiliser qu’en fin de partie et je devais utiliser un autre algorithme, moins bon, pour le début et le milieu de la partie.
Gérard et François m’ont invité à faire un stage pendant les vacances de Noël 1982. Ils ont tenté de m’intéresser à leurs recherches sur la réécriture, mais sans succès. La seule chose que je voulais était utiliser leurs ordinateurs pour implémenter mon algorithme pour jouer au Master Mind. Et ils m’ont laissé faire. Cela m’a permis d’avoir de bien meilleurs résultats et de finir avec le 3ème prix, cette fois au niveau européen.
Durant ce stage, Gérard m’avait quand même expliqué qu’il n’y avait pas d’algorithme pour décider si un programme terminait ou non ; il m’a juste dit que c’était un théorème, sans m’en donner la démonstration. Mais cela me semblait incroyable. À l’époque, pour moi, l’informatique se résumait à écrire des programmes ; je voyais cela comme une forme d’artisanat. Ce théorème m’ouvrait de nouveaux horizons : l’informatique devenait une vraie science, avec des résultats, et même des résultats négatifs. C’est ce qui m’a fait changer de projet professionnel.
Gérard m’avait aussi dit que, pour si je voulais vraiment être chercheur et avoir un poste, je devais faire des études. Alors j’ai fait des études, prépa puis école d’ingénieur. Je suis retourné chez Gérard Huet, pour mon stage de recherche de fin d’étude, puis pour ma thèse. Ensuite, je suis devenu professionnel de la recherche ; j’ai eu un poste et j’ai obtenu le grand plaisir de gagner ma vie en faisant ce qui m’intéressait et qui, le plus souvent, qui me procure toujours une très grande joie.
Binaire : Peux-tu nous parler de ta recherche ?
GD : En thèse, je cherchais des algorithmes de démonstration automatique pour produire des démonstrations dans un système qui est devenu aujourd’hui le système Coq. Mais dans les conférences, je découvrais que d’autres gens développaient d’autres systèmes de vérification de démonstrations, un peu différents. Cela me semblait une organisation curieuse du travail. Chacun de son côté développait son propre système, alors que les mathématiques sont, par nature, universelles.
Qu’est-ce qu’un système de vérification de démonstrations mathématiques ? Prouver un théorème n’est pas facile. En fait, comme l’ont montré Church et Turing, il n’existe pas d’algorithme qui puisse nous dire, quand on lui donne un énoncé, si cet énoncé a une démonstration ou non. En revanche, si, en plus de l’énoncé du théorème, on donne une démonstration potentielle de cet énoncé, il est possible de vérifier avec un algorithme que la démonstration est correcte. Trouver des méthodes pour vérifier automatiquement les démonstrations mathématiques était le programme de recherche de Robin Milner (Prix Turing) et également de Nicolaas De Bruijn. Mais en faisant cela, ils se sont rendu compte que si on voulait faire vérifier des démonstrations par des machines, il fallait les écrire très différemment, et beaucoup plus rigoureusement, que la manière dont on les écrit habituellement pour les communiquer à d’autres mathématiciens.
Les travaux de Milner et de De Bruijn ouvraient donc une nouvelle étape dans l’histoire de la rigueur mathématique, comme avant eux, ceux d’Euclide, de Russell et Whitehead et de Bourbaki. Le langage dans lequel on exprime les démonstrations devient plus précis, plus rigoureux. L’utilisation de logiciels change la nature même des mathématiques en créant, par exemple, la possibilité de construire des démonstrations qui font des millions de pages.
Notre travail était passionnant mais je restais insatisfait par le côté tour de Babel : chaque groupe arrivait avec son langage et son système de vérification. Est-ce que cela impliquait à un relativisme de la notion de vérité ? Il me semblait que cela conduisait à une crise de l’universalité de la vérité mathématique. Ce n’était certes pas la première de l’histoire, mais les crises précédentes avaient été résolues. J’ai donc cherché à construire des outils pour résoudre cette crise-là.
Binaire : Est-ce qu’on ne rencontre pas un problème assez semblable avec les langages de programmation ? On a de nombreuses propositions de langages.
GD : Tout à fait. Cela tient à la nature même des langages formels. Il faut faire des choix dans la manière de s’exprimer. Pour implémenter l’algorithme de l’addition dans un langage de programmation (ajouter les unités avec les unités, puis les dizaines avec les dizaines, etc. en propageant la retenue), on doit décider comment représenter les nombres, si le symbole « etc. » traduit une boucle, une définition par récurrence, une définition récursive, etc. Mais pour les langages de programmation, il y a des traducteurs (les compilateurs) pour passer d’un langage à un autre. Et on a un avantage énorme : tous les langages de programmation permettent d’exprimer les mêmes fonctions : les fonctions calculables.
Avec les démonstrations mathématiques, c’est plus compliqué. Tous les langages ne sont pas équivalents. Une démonstration particulière peut être exprimable dans un langage mais pas dans un autre. Pire, il n’y a pas de langage qui permette d’exprimer toutes les démonstrations : c’est une conséquence assez simple du théorème de Gödel. Peut-on traduire des démonstrations d’un langage vers un autre ? Oui, mais seulement partiellement.
Pour résoudre une précédente crise de l’universalité de la vérité mathématique, la crise des géométries non euclidiennes (*), Hilbert et Ackermann avaient introduit une méthode : ils avaient mis en évidence que Euclide, Lobatchevski et Riemann n’utilisaient pas les mêmes axiomes, mais surtout ils avaient proposé un langage universel, la logique des prédicats, dans lequel ces différents axiomes pouvaient s’exprimer. Cette logique des prédicats a été un grand succès des mathématiques des années 1920 et 1930 puisque, non seulement les différentes géométries, mais aussi l’arithmétique et la théorie des ensembles s’exprimaient dans ce cadre. Mais, rétrospectivement, on voit bien qu’il y avait un problème avec la logique des prédicats, puisque personne n’avait exprimé, dans ce cadre logique, la théorie des types de Russell, une autre théorie importante à cette époque. Et pour le faire, il aurait fallu étendre la logique des prédicats. Par la suite, de nombreuses autres théories ont été proposées, en particulier le Calcul des Constructions, qui est le langage du système Coq, et n’ont pas été exprimée dans ce cadre.
Au début de ma carrière, je pensais qu’il suffisait d’exprimer le Calcul des Constructions dans la logique des prédicats pour sortir de la tour de Babel et retrouver l’universalité de la vérité mathématique. C’était long, pénible, frustrant, et en fait, cette piste m’a conduit à une impasse. Mais cela m’a surtout permis de comprendre que nous avions besoin d’autres cadres que la logique des prédicats. Et, depuis les années 1980, plusieurs nouveaux cadres logiques étaient apparus dans les travaux de Dale Miller, Larry Paulson, Tobias Nipkow, Bob Harper, Furio Honsel, Gordon Plotkin, et d’autres. Nous avons emprunté de nombreuses idées à ces travaux pour aboutir à un nouveau cadre logique que nous avons appelé Dedukti (“déduire” en espéranto). C’est un cadre général, c’est-à-dire un langage pour définir des langages pour exprimer des démonstrations. En Dedukti, on peut définir par exemple la théorie des types de Russell ou le Calcul des Constructions et on peut mettre en évidence les axiomes utilisés dans chaque théorie, et surtout dans chaque démonstration.
Binaire : Pourquoi l’appeler Dedukti ? Ce n’est pas anodin ?
GD : Qu’est-ce qui guidait ces travaux ? L’idée que certaines choses, comme la vérité mathématique, sont communes à toute l’humanité, par-delà les différences culturelles. Nous étions attachés à cette universalité des démonstrations mathématiques, les voir comme des “communs”. Dans l’esprit, les liens avec des communs numériques comme les logiciels libres sont d’ailleurs étroits. On retrouve les valeurs d’universalité et de partage. Il se trouve d’ailleurs que la plupart des systèmes de vérification de démonstrations sont des logiciels libres. Coq et Dedukti le sont. Vérifier une démonstration avec un système qu’on ne peut pas lui-même vérifier, parce que son code n’est pas ouvert, ce serait bizarre.
Revenons sur cette universalité. Si quelqu’un arrivait avec une théorie et qu’on n’arrivait pas à exprimer cette théorie dans Dedukti, il faudrait changer Dedukti, le faire évoluer. Il n’est pas question d’imposer un seul système, ce serait brider la créativité. Ce qu’on vise, c’est un cadre général qui englobe tous les systèmes de vérification de démonstrations utilisés.
Longtemps, nous étions des gourous sans disciples : nous avions un langage universel, mais les seuls utilisateurs de Dedukti étaient l’équipe de ses concepteurs. Mais depuis peu, Dedukti commence à avoir des utilisateurs extérieurs à notre équipe, un peu partout dans le monde. C’est bien entendu une expansion modeste, mais cela montre que nos idées commencent à être comprises et partagées.
Binaire : Tu es très intéressé par les langages formels. Tu as même écrit un livre sur ce sujet. Pourrais-tu nous en parler ?
GD : Les débutants en informatique découvrent d’abord les langages de programmation. L’apprentissage d’un langage de programmation n’est pas facile. Mais la principale difficulté de cet apprentissage vient du fait que les langages de programmation sont des langages. Quand on s’exprime dans un langage, il faut tout dire, mais avec un vocabulaire et une syntaxe très pauvre. Les langages de démonstrations sont proches des langages de programmation. Mais de nombreux autres langages formels sont utilisés en informatique, par exemple des langages de requêtes comme SQL, des langages de description de pages web comme HTML, et d’autres. Le concept de langage formel est un concept central de l’informatique.
Mais ce concept a une histoire bien plus ancienne que l’informatique elle-même. Les humains ont depuis longtemps inventé des langages dans des domaines particuliers, comme les ophtalmologistes pour prescrire des lunettes. On peut multiplier les exemples : en mathématiques, les langages des nombres, de l’arithmétique, de l’algèbre, où apparaît pour la première fois la notion de variable, les cylindres à picots des automates, le langage des réactions chimiques, inventé au XIXe siècle, la notation musicale.
C’est le sujet de mon livre, Ce dont on ne peut parler, il faut l’écrire (Le Pommier, 2019). La création de langage est un énorme champ de notre culture. Les langages sont créés de toute pièce dans des buts spécifiques. Ils sont bien plus simples que les langues naturelles utilisées à l’oral. Ils expriment moins de choses mais ils sont souvent au centre des progrès scientifiques. L’écriture a probablement été inventée d’abord pour fixer des textes exprimés dans des langages formels et non dans des langues.
Binaire : Tu fais une très belle recherche, plutôt fondamentale. Est-ce que faire de la recherche fondamentale sert à quelque chose ?
GD : Je ne sais pas si je fais de la recherche fondamentale. En un certain sens, toute l’informatique est appliquée.
Maintenant, est-ce que la recherche fondamentale sert à quelque chose ? Cela me rappelle une anecdote. À l’École polytechnique, le poly d’informatique disait que la moitié de l’industrie mondiale était due aux découvertes de l’informatique et celui de physique que deux tiers de l’industrie mondiale étaient dus aux découvertes de la physique quantique. Les élèves nous faisaient remarquer que 1/2 + 2/3, cela faisait plus que 1. Bien entendu, les physiciens avaient compté toute l’informatique dans la partie de l’industrie que nous devions à la physique quantique, car sans physique quantique, pas de transistors, et sans transistors, pas d’informatique. Mais le message commun que nous voulions faire passer était que des pans entiers de l’économie existent du fait de découvertes scientifiques au départ perçues comme fondamentales. L’existence d’un algorithme pour décider de la correction d’une démonstration mathématique, question qui semble très détachée de l’économie, nous a conduit à concevoir des logiciels plus sûrs. La recherche la plus désintéressée, éloignée a priori de toute application, peut conduire à des transformations majeures de l’économie.
Cependant, ce n’est pas parce que la recherche a une forte influence sur le développement économique que nous pouvons en conclure que c’est sa seule motivation. La recherche nous sert aussi à mieux comprendre le monde, à développer notre agilité intellectuelle, notre esprit critique, notre curiosité. Cette quête participe de notre humanité. Et si cela conduit à des progrès industriels, tant mieux.
Serge Abiteboul, Inria, & Claire Mathieu, CNRS
(*) Des géomètres comme Euclide ont démontré que la somme des angles d’un triangle est toujours égale à 180 degrés. Mais des mathématiciens comme Lobatchevski ont démontré que cette somme était inférieure à 180 degrés. Crise ! Cette crise a été résolue au début du XXe siècle par l’observation, finalement banale, que Euclide et Lobatchevski n’utilisaient pas les mêmes axiomes, les mêmes présupposés sur l’espace géométrique.
https://www.lemonde.fr/blog/binaire/les-entretiens-de-la-sif/
