Un nouvel « entretien autour de l’informatique ». Serge Abiteboul et Claire Mathieu interviewent Gérard Huet , Directeur de recherche émérite à Inria. Gérard Huet a apporté des contributions fondamentales à de nombreux sujets de l’informatique, démonstration automatique, unification, édition structurée, réécriture algébrique, calcul fonctionnel, langages de programmation applicatifs, théorie des types, assistants de preuve, programmation relationnelle, linguistique computationnelle, traitement informatique du sanskrit, lexicologie, humanités numériques, etc. Ses travaux sur CAML et Coq (voir encadrés en fin d’article) ont notamment transformé de manière essentielle l’informatique.
B : Tu as eu un parcours de chercheur singulier, avec des contributions fondamentales dans un nombre incroyable de sujets de l’informatique. Est-ce qu’il y a des liens entre tous tes travaux ?
G : Il existe des liens profonds entre la plupart de ces sujets, notamment une vision du cœur de la discipline fondée sur l’algèbre, la logique et les mathématiques constructives. Le calcul fonctionnel (le lambda-calcul dans le jargon des théoriciens) sous-tend nombre d’entre eux. Le calcul fonctionnel, pour simplifier, c’est une théorie mathématique avec des fonctions qui ne s’appliquent pas juste à des réels comme celles que vous avez rencontrées en cours de maths. Ces fonctions, ou plus précisément ces algorithmes, peuvent s’appliquer à d’autres objets et notamment à des objets fonctionnels. Vous pouvez avoir une fonction qui trie des objets. Vous allez passer comme argument à cette fonction une autre fonction qui permet de comparer l’âge de deux personnes et vous obtenez une fonction qui permet de trier un ensemble de personnes par ordre d’âge.
Ce qui montre que ce calcul fonctionnel est une notion fondamentale, c’est à la fois l’ossature des programmes informatiques, et dans sa version typée la structure des démonstrations mathématiques (la déduction naturelle dans le jargon des logiciens). Vous n’avez pas besoin de comprendre tous les détails. La magie, c’est que le même objet mathématique explique à la fois les programmes informatiques et les preuves mathématiques. Il permet également les représentations linguistiques à la fois de la syntaxe, du discours, et du sens des phrases de la langue naturelle (les grammaires de Lambek et les grammaires de Montague dans le jargon des linguistes). Reconnaître cette unité est un puissant levier pour appliquer des méthodes générales à plusieurs champs applicatifs.
Je suis tombé sur d’autres sujets au fil de hasards et de rencontres parfois miraculeuses.
Les programmes sont des preuves constructives
B : Les programmes sont des preuves. Ça te paraît évident mais ça ne l’est pas pour tout le monde. Pourrais-tu nous expliquer comment on est arrivé à ces liens entre programmes et preuves ?
G : Tout commence avec la logique mathématique. En logique, il y a deux grandes familles de systèmes de preuves. La première, la déduction naturelle, avec des arbres de preuves, c’est comme le lambda-calcul typé, et les propositions de la logique sont les types des formules de lambda-calcul. Ce n’est pas quelque chose qui a été compris au début. Le livre standard sur la déduction naturelle, paru en 1965, ne mentionne même pas le λ calcul, car l’auteur n’avait pas vu le rapport. C’est dans les années 70, qu’on a découvert qu’on avait développé deux théories mathématiques équivalentes, chacun des deux domaines ayant développé des théorèmes qui en fait étaient les mêmes. Quand on fait le pont entre les deux, on comprend que, les programmes, ce sont des preuves.
En mathématiques, on raisonne avec des axiomes et des inférences pour justifier la démonstration des théorèmes, mais souvent on évacue un peu la preuve elle-même en tant qu’objet mathématique en soi. La preuve, pour un mathématicien, c’est comme un kleenex : on la fait, et puis ça se jette. La preuve passe, le théorème reste. D’ailleurs, on donne aux théorèmes des noms de mathématiciens, mais, les preuves, on s’en moque. Ça, c’est en train de changer grâce à l’informatique. Pour nous, les preuves sont des objets primordiaux. Plus précisément, ce qui est important pour nous, ce sont les algorithmes. En effet, un théorème peut avoir plusieurs preuves non équivalentes. L’une d’entre elles peut ne pas être constructive, c’est à dire par exemple montrer qu’un objet existe sans dire comment le construire. Ça intéresse moins l’informaticien. Les autres preuves donnent des constructions. Ce sont des algorithmes. Un théorème dit par exemple que si on a un ensemble d’objets que l’on peut trier, alors on peut construire une séquence triée de ces objets. C’est un théorème – il est complètement trivial pour un mathématicien. Mais pour nous pas du tout. Si vous voulez trier un million d’enregistrements, vous aimeriez que votre algorithme soit rapide. Alors les informaticiens ont développé de nombreux algorithmes pour trier des objets qu’ils utilisent suivant les contextes, des preuves différentes de ce théorème trivial qui sont plus utiles qu’une preuve non constructive. Et ce sont de beaux objets !
Voilà, quand on a compris qu’un algorithme c’est une preuve, on voit bien que plusieurs algorithmes peuvent avoir la même spécification et donc que la preuve importe.
B : La mode aujourd’hui est d’utiliser le mot « code » pour parler de programmes informatiques. Tu ne parles pas de code ?
G : Au secours ! Le mot « code » est une insulte à la beauté intrinsèque de ces objets. La représentation d’un entier sous forme de produit de nombres premiers, on ne doit pas appeler cela un « codage » ! Non, cette représentation des entiers est canonique, et découle du Théorème Fondamental de l’Arithmétique. C’est extrêmement noble. Dans le terme « codage », il y a l’idée de cacher quelque chose, alors qu’au contraire, il s’agit de révéler la beauté de l’objet en exhibant l’algorithme.
L’esthétique des programmes
B : Les gens voient souvent les programmes informatiques comme des suites de symboles barbares, des trucs incompréhensibles. C’est beaucoup pour cela que le blog binaire milite pour l’enseignement de l’informatique, pour que ces objets puissent être compris par tous. Mais tu as dépassé l’état de le compréhension. Tu nous parles d’esthétique : un programme informatique peut-il être beau ?
GH : Bien sûr. Son rôle est d’abord d’exposer la beauté de l’algorithme sous-jacent. L’esthétique, c’est plus important qu’il n’y paraît. Elle a des motivations pratiques, concrètes. D’abord, les programmes les plus beaux sont souvent les plus efficaces. Ils vont à l’essentiel sans perdre du temps dans des détails, des circonvolutions inutiles. Et puis un système informatique est un objet parfois très gros qui finit par avoir sa propre vie. Les programmeurs vont et viennent. Le système continue d’être utilisé. La beauté, la lisibilité des programmes est essentielle pour transmettre les connaissances qui s’accumulent dans ces programmes d’une génération de programmeurs à l’autre qui ont comme mission de pérenniser le fonctionnement du système.
Pour les programmes, de même que pour les preuves, il ne faut jamais se satisfaire du premier jet. On est content quand ça marche, bien sûr, mais c’est à ce moment là que le travail intéressant commence, qu’on regarde comment nettoyer, réorganiser le programme, et c’est souvent dans ce travail qu’on découvre les bonnes notions. On peut avoir à le réécrire tout ou en partie, l’améliorer, le rendre plus beau.
Prenez le cas d’Unix (*). Unix, c’est beau, c’est très beau ! Il faut savoir voir Unix comme une très grande œuvre d’art. Unix a été réalisé dans le laboratoire de recherche de Bell, par une équipe de chercheurs. Vaughan Pratt (+) disait dans les années 80 :« Unix, c’est le troisième Testament ». Vaughan Pratt, c’est quelqu’un d’incroyable ! Il ne dit pas n’importe quoi (rire de Gérard). Eh bien, Unix a été fait dans une équipe de spécialistes de théorie des langages et des automates. C’est une merveille de systèmes communiquant par des flots d’octets, tout simplement. C’est minimaliste. Ils ont pris le temps qu’il fallait, ils ont recherché l’élégance, la simplicité, l’efficacité. Ils les ont trouvées !
B : Parmi tes nombreux travaux, y en a-t-il un qui te tient particulièrement à cœur ?
GH : Je dirais volontiers que mon œuvre préférée, c’est le « zipper ». C’est une technique de programmation fonctionnelle. Elle permet de traverser des structures de données les plus utilisées en informatique comme des listes et des arbres pour mettre à jour leur contenu.
Le zipper (voir aussi la page), je suis tombé dessus pour expliquer comment faire des calculs applicatifs sur des structures de données, sans avoir cette espèce de vision étroite de programmation applicative où, pour faire des remplacements dans une structure de données, tu gardes toujours le doigt sur le haut de ta structure, ton arbre, et puis tu te balades dedans, mais tu continues à regarder ta structure d’en haut. Le zipper, au lieu de cela, tu rentres dans la structure, tu vis à l’intérieur, et alors, ce qui compte, c’est d’une part l’endroit où tu es, et d’autre part le contexte qui permet de te souvenir de comment tu es arrivé là. C’est une structure fondamentale qui avait totalement échappé aux informaticiens. Des programmeurs faisaient peut-être bien déjà du zipper sans le savoir comme M. Jourdain faisait de la prose. J’ai su formaliser le concept en tant que structure de donnée et algorithmes pour la manipuler. Maintenant, on peut enseigner le zipper, expliquer son essence mathématique.
La mystique de la recherche
B : Qu’est-ce qui est important pour réussir une carrière en recherche ?
GH : Le plus important finalement, dans le choix du sujet de recherche, ce sont trois choses : le hasard, la chance, et les miracles. Je m’explique. Premièrement, le hasard. Il ne se contrôle pas. Deuxièmement, la chance. C’est d’être au bon moment au bon endroit, mais surtout de savoir s’en apercevoir et la saisir.
Par exemple, dans le Bâtiment 8 (++) où je travaillais à l’INRIA Rocquencourt, il passait beaucoup de visiteurs. Le hasard c’est un jour la visite de Corrado Böhm , un des maîtres du lambda-calcul, une vraie encyclopédie du domaine. Je lui explique ce que je fais, et il me conseille de lire un article qui était alors, en 1975, inconnu de presque tous les informaticiens : c’était l’algorithme de Knuth-Bendix. C’est un résultat majeur d’algèbre constructive permettant de reformuler des résultats d’algèbre de manière combinatoire. La chance, j’ai su la saisir. J’ai vu tout de suite que c’était important. Cela m’a permis d’être un précurseur des systèmes de réécriture un peu par ce hasard. Voilà, j’ai su saisir ma chance. On se rend compte qu’il y a quelque chose à comprendre, et on creuse. Donc il faut être en éveil, avoir l’esprit assez ouvert pour regarder le truc et y consacrer des efforts.
À une certaine époque, j’étais un fréquent visiteur des laboratoires japonais. Une fois, je suis resté une quinzaine de jours dans un laboratoire de recherche. Je conseillais aux étudiants japonais d’être en éveil, d’avoir l’esprit ouvert. Je leurs répétais : « Be open-minded! ». Ils étaient étonnés, et mal à l’aise de questionner les problèmes qui leur avaient été assignés par leur supérieur hiérarchique. Un an plus tard, je suis repassé dans le même labo. Ils avaient gardé ma chaise à une place d’honneur, et ils l’appelaient (rire de Gérard) « the open-mindedness chair » !
B : Esthétique, miracle, troisième testament… Il y aurait une dimension mystique à ton approche de la recherche ?
GH : En fait, souvent, derrière les mystères, il y a des explications. Un exemple : je suis parti aux USA sur le mirage de l’intelligence artificielle. Une fois là-bas, quelle déception. J’ai trouvé qu’en intelligence artificielle, la seule chose qui à l’époque avait un peu de substance, c’était la démonstration automatique. J’ai essayé. Et puis, j’ai fait une croix dessus car cela n’aboutissait pas. Cela semblait inutile, et je voulais faire des choses utiles. Alors j’ai regardé ailleurs, des trucs plus appliqués comme les blocages quand on avait des accès concurrents à des ressources. Par hasard, je suis tombé sur deux travaux. Le premier, un article de Karp et Miller, m’a appris ce que c’était que le Problème de Correspondance de Post (PCP), un problème qui est indécidable – il n’existe aucun algorithme pour le résoudre. Le second était une thèse récemment soutenue à Princeton qui proposait un algorithme pour l’unification d’ordre supérieur. Je ne vais pas vous expliquer ces deux problèmes, peut-être dans un autre article de Binaire. L’algorithme de la thèse, je ne le comprenais pas bien. Surtout, ça ne m’intéressait pas trop, car c’était de la démonstration automatique et je pensais en avoir fini avec ce domaine. Eh bien, un ou deux mois plus tard, je rentre chez moi après une soirée, je mets la clé dans la serrure de la porte d’entrée, et, paf ! J’avais la preuve de l’indécidabilité de l’unification d’ordre supérieur en utilisant le PCP. J’avais établi un pont entre les deux problèmes. Bon ça montrait aussi que le résultat de la thèse était faux. Mais ça arrive, les théorèmes faux. Pour moi, quel flash ! J’avais résolu un problème ouvert important. Quand je parle de miracle, c’est quelque chose que je ne sais pas expliquer. J’étais à mille lieues de me préoccuper de science, et je ne travaillais plus là dessus. C’est mon inconscient qui avait ruminé sur ce problème du PCP, et c’est un cheminement entièrement inconscient qui a fait que la preuve s’est mise en place. Mais il faut avoir beaucoup travaillé pour arriver à ça, avoir passé du temps à lire, à comprendre, à essayer des pistes infructueuses, à s’imprégner de concepts que l’on pense important, à comprendre des preuves. C’est beaucoup de travail. La recherche, c’est une sorte de sacerdoce.
Bon, il faut aussi savoir s’arrêter, ne pas travailler trop longtemps sur un même problème. Faire autre chose. Sinon, eh bien on devient fou.
| Caml (prononcé camel, signifie Categorical Abstract Machine Language) est un langage de programmation généraliste conçu pour la sécurité et la fiabilité des programmes. Descendant de ML, c’est un langage de programmation directement inspiré du calcul fonctionnel, issu des travaux de Peter Landin et Robin Milner. À l’origine simple langage de commandes d’un assistant à la preuve (LCF), il fut développé à l’INRIA dans l’équipe Formel sous ses avatars de Caml puis d’OCaml. Les auteurs principaux sont Gérard Huet, Guy Cousineau, Ascánder Suárez, Pierre Weis, Michel Mauny pour Caml ; Xavier Leroy, Damien Doligez et Didier Rémy et Jérôme Vouillon pour OCaml. |
| Coq est un assistant de preuve 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 preuves de ces affirmations, et aide à trouver des preuves 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. |
(*) Unix : Unix est un système d’exploitation multitâche et multi-utilisateur créé en 1969. On peut le voir comme l’ancêtre de systèmes aussi populaires aujourd’hui que Linux, Android, OS X et iOS.
(+) Vaughan Pratt est avec Gérard Huet un des grands pionniers de l’informatique. Il a notamment dirigé le projet Sun Workstation, à l’origine de la création de Sun Microsystems.
(++) Bâtiment 8 ; Bâtiment quasi mythique d’Inria (de l’IRIA ou de l’INRIA) Rocquencourt pour les informaticiens français, qui a vu passer des chercheurs disparus comme Philippe Flajolet et Gilles Kahn, et de nombreuses autres stars de l’informatique française toujours actifs, souvent à l’instigation de Maurice Nivat. Gilles Kahn sur la photo était une sorte de chef d’orchestre, parmi un groupe de chercheurs plutôt anarchistes dans leur approche de la recherche.
De la complexité du problème : Les contraintes entre les variables, © Openfisca
Mettre au point un système de vote électronique sûr est un exercice délicat. En particulier, la vérifiabilité et la résistance à la coercition sont des propriétés antagonistes : il faut à la fois démontrer qu’un certain vote a été inclus dans le résultat et ne pas pouvoir montrer à un tiers comment on a voté.
