Langages des maths, langages de l’informatique
Entretien avec Thierry Coquand, informaticien et mathématicien français, professeur à l'Université de Göteborg en Suède.
Un nouvel « entretien autour de l’informatique ». Serge Abiteboul et Gilles Dowek interviewent Thierry Coquand, informaticien et mathématicien français, professeur à l’Université de Göteborg en Suède. Thierry Coquand est l’auteur de nombreux travaux en théorie de la démonstration et sur les mathématiques constructives. Il est, en particulier, à l’origine, avec Gérard Huet, du Calcul des constructions, qui est la théorie implémentée dans le système Coq (voir encadré en fin d’article). B : tes travaux se situent à la frontière de l’informatique et des mathématiques. Est-ce que ce sont pour toi deux domaines distincts ? TC : le point de départ de ma thèse était une tentative d’identifier ces deux domaines. Avec le recul, je me rends compte de la naïveté de ce projet. Cependant, il existe des analogies remarquables entre les deux domaines, qui nous apprennent énormément sur l’un et sur l’autre, et c’est cela qui m’intéresse. B : peux-tu nous parler d’une de ces analogies que tu as étudiée dans ta thèse ? TC : dans ma thèse, je me suis intéressé au raisonnement mathématique et à sa représentation sur un ordinateur. L’étude du raisonnement est ancienne, mais l’arrivée de l’informatique l’a bouleversée, car il devenait possible de confier à une machine la vérification de la correction des raisonnements. Avant la rencontre avec l’informatique, les mathématiciens, notamment Bourbaki, étaient déjà allés très loin sur le chemin de la formalisation des démonstrations, mais ils voyaient bien les limites de cette démarche. Si on donne tous les détails dans une démonstration, si on la formalise totalement, elle devient vite trop longue et illisible pour les humains. En revanche, un ordinateur a besoin de tous ces détails et ne s’effraie pas de la longueur des démonstrations. L’arrivée de l’informatique changeait donc tout. J’ai été influencé par les travaux du mathématicien néerlandais, Nicolaas de Bruijn, qui a eu l’idée d’utiliser des notations issues de l’informatique pour représenter les démonstrations. Ses travaux, ceux du statisticien et logicien suédois Per Martin-Löf et du logicien français Jean-Yves Girard m’ont beaucoup influencé. Ma thèse fait la synthèse des langages qu’ils ont proposés. On retrouve dans nos travaux, l’idée que les démonstrations mathématiques sont des programmes exprimés dans un type particulier de langage de programmation : un langage fonctionnel, comme les langages Lisp ou ML. Cette manière d’exprimer les programmes est particulièrement appropriée pour obtenir une représentation uniforme des programmes informatiques et des démonstrations mathématiques. La programmation fonctionnelle apporte comme une correspondance magique entre programmes et démonstrations. C’est ce que j’ai fait dans ma thèse. Et c’est le programme que j’ai poursuivi pendant trente ans dans un domaine qui reste toujours très riche. Cette correspondance entre programmes fonctionnels et démonstrations jette rétrospectivement une lumière nouvelle sur les travaux des logiciens des années 1930, par exemple ceux de Gerhard Gentzen, qui y trouve en quelque sorte les bons langages pour être exprimés. On peut aussi s’intéresser à la généralisation de cette correspondance à d’autres types de langages de programmation. C’est une direction de recherche active aujourd’hui. B : le langage pour décrire des algorithmes ou des démonstrations. C’est bien le sujet ? TC : on connaît depuis longtemps l’importance des notations en mathématiques. J’aime bien l’exemple de Leibniz. Une de ses grandes contributions pour le calcul différentiel tient dans les notations qu’il introduit. De Bruijn aussi a passé beaucoup de temps à comprendre ce que sont les bonnes notations en logique et en mathématique. L’informatique ici aussi apporte un renouveau : parce que les systèmes qu’ils conçoivent sont très complexes, les informaticiens sont obligés de trouver de bonnes notations. B : la manière d’exprimer les démonstrations évolue avec le temps, n’est-ce pas contradictoire avec l’idée d’objectivité de la vérité mathématique ? La correction d’un raisonnement mathématique doit être un fait objectif. Mais le chemin vers la perfection est long et ce que nous avons découvert, depuis cinquante ans est qu’écrire des démonstrations absolument correctes est impossible sans ordinateur. Chaque étape du développement des mathématiques nous a cependant apporté de nouvelles notations qui nous ont rapproché de cet idéal. C’est pour cela qu’il y a une histoire de des langages d’expression des démonstrations. Il nous reste cependant encore beaucoup de progrès à faire : les démonstrations formelles que nous écrivons aujourd’hui sont difficilement lisibles par les humains. Nous devons donc comprendre comment concilier complexité, correction et lisibilité. Nous ne sommes qu’au début de cette histoire. B : l’informatique également est confrontée à cette complexité ? TC : les informaticiens sont confrontés à la complexité des programmes, de même que les mathématiciens confrontés à celle des démonstrations. Ils ont donc eux aussi besoin de vérifier que leurs programmes sont corrects, qu’ils font bien ce qu’ils sont supposés faire. Les outils pour raisonner sur les programmes, pour vérifier leur correction sont les mêmes que ceux qui permettent de vérifier la correction des démonstrations mathématiques. C’est une autre illustration de cette correspondance fantastique entre programmes et démonstrations. B : peux-tu nous donner un exemple de cette complexité ? Où voit-on des signes d’imperfection dans la représentation formelle des raisonnements ? TC : Georges Gonthier et son équipe ont formalisé une démonstration du théorème de Feit-Thompson. La démonstration de ce théorème était connue depuis les années 1960 mais il leur a fallu six ans pour construire cette démonstration formelle, c’est bien le signe que tout n’était pas dit dans la démonstration originale. La démonstration de Georges nous permet d’avoir véritablement confiance dans ce résultat. Mais au delà, elle nous permet aussi de maîtriser la complexité du problème, de l’analyser, de comprendre sa structure de façon plus fondamentale. À mes yeux, le plus intéressant dans ce tour de force est que pour y arriver il s’est appuyé sur ses intuitions d’informaticien. C’est exactement ce que Gérard Huet et moi avions en tête quand nous avons commencé notre travail sur le Calcul des constructions : l’idée que nos intuitions de mathématiciens étaient utiles pour écrire des programmes et que nos intuitions d’informaticiens étaient symétriquement utiles pour écrire des démonstrations. Ces systèmes de vérification de démonstrations formelles arrivent aussi à un moment particulier de l’histoire des mathématiques. On commence depuis quelques années à voir apparaître des démonstrations de plusieurs centaines de pages. Les mathématiciens s’attaquent aujourd’hui à des démonstrations très complexes qu’il devient quasiment impossible de vérifier « à la main ». B : en astronomie, la lunette permet de dépasser les limites de l’œil ? Les systèmes de vérification de démonstrations sont-ils des outils analogues pour les mathématiciens ? TC : c’est une motivation bien sûr. On peut rêver de proposer aux mathématiciens des outils à la mesure de leurs rêves, des outils qui leurs permettent de dompter la complexité de certaines démonstrations. Mais nous n’en sommes qu’au début. Les mathématiciens ne se sont pas encore emparés de ces logiciels comme les astronomes des télescopes. Peut-être l’outil est-il encore trop récent ? B : l’outil, c’est la programmation fonctionnelle qui permet d’unifier la démonstration mathématique et la programmation. TC : un même outil mathématique, le lambda-calcul, représente remarquablement bien à la fois la structure d’une démonstration mathématique et celle d’un algorithme. C’est ce même objet qui est à l’origine de la programmation fonctionnelle. B : mais peut-on exprimer n’importe quel raisonnement ? TC : dans les années 1900-1930, il y a eu de grands débats en logique. Peut-on démontrer l’existence d’un objet sans jamais montrer cet objet. C’est ce qu’il se passe, par exemple, dans un raisonnement par l’absurde. Si on suppose qu’un tel objet n’existe pas, on arrive à une contradiction. Donc un tel objet existe parce qu’il est impossible qu’il n’existe pas. Dans un tel argument, on ne montre jamais l’objet dont on démontre l’existence. On n’a pas le début d’une idée pour imaginer à quoi il ressemble. Avec le lambda-calcul, on se focalise sur les démonstrations « constructives », celles qui montrent comment construire les objets dont elles montrent l’existence. B : faut-il interdire le raisonnement par l’absurde ? TC : non bien entendu, mais les démonstrations par l’absurde occupent une place singulière au sein des démonstrations. Cette singularité fait qu’ils trouvent mal leur place dans la correspondance entre programmes et démonstrations. Cette correspondance est surtout une correspondance entre les programmes fonctionnels et les démonstrations constructives. Peut-on aller au-delà des démonstrations constructives ? C’est une direction de recherche active aujourd’hui. B : tu as apporté des contributions considérables avec le Calcul des constructions, qui est la base du système Coq. Aujourd’hui sur quoi portent tes travaux ? TC : ma réponse va peut-être surprendre les lecteurs de Binaire. Mais depuis trente ans nous sommes bloqués par une question qui a l’air simple. Qu’est-ce que l’égalité ? Comment définir ce symbole que nous notons « = » ? Les réponses que, depuis Leibniz, nous avons apportées à cette question sont toutes insatisfaisantes. Car elles n’égalisent pas assez d’objets, nous voudrions montrer que tel objet est égal à tel autre, mais nous n’y parvenons pas car notre définition de l’égalité est trop tatillonne. Un grand mathématicien, Vladimir Voevodsky s’est intéressé à la question. Ses démonstrations étaient tellement complexes qu’elles n’étaient pas suffisamment vérifiées. Il s’inquiétait du fait que des erreurs pourraient rester ignorées et a donc cherché à les vérifier en utilisant le système Coq. Il a alors découvert des analogies surprenantes entre la topologie, c’est-à-dire la théorie de la représentation des formes et celle de l’égalité. À côté, de la correspondance entre programmes et démonstrations, apparaissait une nouvelle correspondance entre l’homotopie et l’égalité dans la théorie des types. C’est véritablement remarquable ! B : pourrais-tu nous dévoiler un des secrets de tes succès professionnels ? TC : ce n’est pas un secret : le travail d’équipe. Ce que j’ai fait n’était possible qu’avec les gens qui sont venus avant comme mon directeur de thèse, Gérard Huet, et d’autres pour poursuive les travaux après comme Hugo Herbelin. On bâtit nos résultats sur ceux des autres. J’ai mentionné des travaux qui ont influencé ma recherche. Et leurs impacts ne dépendent pas que de nous. La théorie des constructions n’aurait jamais eu cet impact sans le système Coq, c’est-à-dire plus de 15 ans de travail d’une équipe brillante. B : pourrait-on enseigner cela aux enfants ? TC : j’aimerais que toute cette théorie serve pour enseigner les démonstrations aux enfants. Ce sujet passionnait déjà de Bruijn. La notion de démonstration est difficile à enseigner aux enfants. Qu’est-ce que c’est une démonstration ? Comment peut-on se convaincre qu’elle est correcte ? Est-ce que j’ai donné assez de détail pour convaincre quelqu’un d’autre ? Il me semble qu’enseigner la notion de démonstrations en s’appuyant sur la vérification d’algorithmes est la bonne direction. Il y a par exemple les travaux là-dessus de Julien Narboux à Strasbourg. Les enfants comprennent bien la notion d’algorithme et la proximité des notations entre programmes et démonstrations facilite la tâche. Serge Abiteboul et Gilles Dowek Définitions Programmation fonctionnelle : les langages de programmation fonctionnels forment une famille de langage, dans laquelle un programme n’est pas vu comme la prescription d’une succession d’étapes devant être exécutées l’une après l’autre, mais comme la description d’une fonction qui à chaque argument associe une valeur. La programmation fonctionnelle vient du le lambda-calcul, un langage inventé dans les années 1930, donc avant la construction des premiers ordinateurs, pour exprimer les algorithmes. Des exemples de langages fonctionnels : Lisp, ML, Haskell, OCaml, Scala. Curry-Howard : La correspondance de Curry-Howard, appelée également correspondance de Curry-de Bruijn-Howard, correspondance démonstration/programme ou correspondance formule / type, est une série de résultats à la frontière entre la logique mathématique, l’informatique théorique et la théorie de la calculabilité. Ils établissent des relations entre les démonstrations formelles d’un système logique et les programmes d’un modèle de calcul. Les premiers exemples de correspondance de Curry-Howard remontent à 1958, date à laquelle Haskell Curry remarqua l’analogie formelle entre les démonstrations des systèmes à la Hilbert et la logique combinatoire, puis à 1969 où William Alvin Howard remarqua que les démonstrations en déduction naturelle intuitionniste pouvaient formellement se voir comme des termes du lambda-calcul typé. Coq est un assistant de démonstration fondé au départ sur le Calcul des Constructions (une variété de calcul fonctionnel typé) introduit par Thierry Coquand et Gérard Huet. Il permet l’expression d’assertions mathématiques, vérifie automatiquement les démonstrations de ces affirmations, et aide à trouver des démonstrations formelles. Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chet Murthy, Yves Bertot, Pierre Castéran ont obtenu le prestigieux 2013 ACM Software System Award pour la réalisation de Coq.