La sémantique, c’est romantique

Le 22 avril 2014, c’était la journée de lancement du trimestre Sémantique des preuves et des programmes et mathématiques certifiées.

Les organisateurs Pierre-Louis Curien, Hugo Herbelin, Paul-André Melliès ¹chercheurs au laboratoire PPS, CNRS et Université Paris 7 proposent, lors de cette après-midi, une sorte de mise en bouche, une bande-annonce de ce dont il va être question jusqu’au mois de juillet à l’IHP.

---

qui constitue la première grosse brique de la classification des groupes finis simples⁴En rapport avec les groupes finis simples, on peut recommander le livre La symétrie ou les maths au clair de lune, de Marcus du Sautoy Editions Héloïse d’Ormesson, 2012. Pour ce faire, Gonthier et ses collaborateurs ont dû alimenter Coq avec les rudiments de l’algèbre, une tâche considérable, mais qui n’exigeait pas une expertise particulière en algèbre. Il y a un point sur lequel l’équipe a dû développer un bout de théorie mathématique nouvelle. La démonstration classique s’appuie sur les nombres complexes, et sur le fameux

Cette construction incorpore une forme de raisonnement par l’absurde qui, pour des raisons historiques, n’est pas autorisée par le langage Coq. Gonthier conclut que l’assistant de preuve apporte une aide considérable au débutant qui cherche à comprendre, et que la formalisation fait progresser le sujet sur le fond.

Hugo Herbelin et Tom Hales

Vers une formalisation de la solution de la conjecture de Kepler ? Il semble que la formule \(\frac{n(n+1)(n+2)}{6}\) pour le nombre d’oranges dans un empilement de hauteur \(n\) est connue depuis plus de 2000 ans.

Pourtant, c’est seulement en 1611, sous la plume de Johannes Kepler, qu’on voit posée la question de savoir si la disposition usuelle des oranges est la meilleure possible, c’est-à-dire qu’on met ainsi le plus d’oranges possible dans un volume donné. La réponse, positive, donnée par Tom Hales et son élève Sam Ferguson (université de Pittsburgh) en 1999 remplit un livre de 300 pages particulièrement aride, avec du logiciel pour traiter plus de 100000 configurations particulières. Bien qu’elle ait été publiée en 2006, personne n’a pu la vérifier entièrement. Depuis le début des années 2000, Hales élabore progressivement une démonstration certifiée, écrite dans le langage HOL-Light. Il a choisi ce langage en raison de sa simplicité : le coeur du logiciel tient en 3 pages, et le langage lui-même a été certifié. Le message de Hales est que, maintenant qu’on dispose d’assistants de preuve, on ne devrait plus considérer la longueur des démonstrations comme un obstacle aux avancées de l’esprit humain. C’est une belle façon de mettre fin à la querelle sur la validité des démonstrations assistées par ordinateur.

Assistants de preuve dans la recherche en informatique Les assistants de preuve ont-ils atteint un degré de maturité qui les rend capables de satisfaire le besoin de la société pour des logiciels certifiés ? C’est-à-dire, des programmes d’ordinateurs dont on peut démontrer qu’ils font exactement ce qu’on pense qu’ils font. Dans ce domaine, il y a encore pas mal de travail à faire. En effet, c’est bien de certifier le programme. Encore faut-il que l’ordinateur sur lequel il tourne fonctionne comme on l’attend. Or il existe une batterie de tests qui vérifie l’arithmétique de base (les 4 opérations) des compilateurs. Aucun des compilateurs commercialisés ne passe la totalité des tests. La raison est que ces compilateurs incorporent d’innombrables astuces accélérant le calcul, c’est là que des erreurs ont été introduites.

Xavier Leroy

Xavier Leroy (INRIA Rocquencourt) et ses collaborateurs ont écrit un nouveau compilateur pour microprocesseurs de la gamme x86, certifié au moyen de Coq. Il passe tous les tests avec succès. Avec 100000 lignes de code, c’est un travail considérable. Il ne faut pas s’arrêter là : les systèmes d’exploitation eux-mêmes ont besoin d’être certifiés. Une équipe australienne, NICTA, a élaboré une version certifiée d’un micro-système d’exploitation, seL4, qui conserve 80% de la puissance de l’original. Les applications industrielles du logiciel certifié ont fait l’objet d’une journée le 28 avril, mais je n’y étais pas.

Paul-André Melliès

Fondements des mathématiques Pour le lien entre certification et fondements des mathématiques, via la toute nouvelle théorie homotopique des types, je renvoie à l’article d’Antoine Chambert-Loir. Vladimir Voevodsky (IAS Princeton), l’un des principaux acteurs de cette théorie, nous dit où il en est. Son objectif à long terme est de bâtir des assistants de preuve que le mathématicien pourrait utiliser, non pas après coup, pour s’assurer que l’enchaînement des raisonnements est correct, mais au fur et à mesure de la création de la démonstration, comme un guide. Cela passe par une refondation formelle des mathématiques, dans laquelle les ensembles sont remplacés par les types, et un axiome d’univalence (mystérieux pour moi) joue un rôle crucial. Cette construction est en cours, certaines bibliothèques écrites en Coq, HoTT et UniMath, en exploitent déjà les idées. Une des difficultés rencontrées est la cohérence. Du point de vue mathématique, on aurait besoin de parler du ∞-groupoïde de tous les ∞-groupoïdes, qui ne peut exister. Du point de vue informatique, cette impossibilité signifie qu’il doit exister des démonstrations correctes que l’assistant de preuve ne peut vérifier (en revanche, on tient à ce que toutes les démonstrations certifiées par l’assistant de preuve soient correctes). L’opinion de Voevodsky est qu’on doit accepter l’incohérence, quitte à rechercher plusieurs niveaux de qualité pour les assistants de preuve (des versions rapides mais très peu cohérentes, des versions plus lentes mais qui parviennent à traiter davantage de démonstrations).

Ce qui m’a frappé dans l’exposé de Voevodsky, c’est sa façon spontanée de s’adresser aux informaticiens, comme si la distance (et le décalage dans le temps) entre la conception d’une théorie très abstraite et la mise en service opérationnelle de langages de programmation qui s’en inspirent était abolie. Comme le montre la parution immédiate du livre issu de la période spéciale consacrée au sujet l’an dernier à Princeton, il semble bien que le temps s’accélère.

A quand une rubrique Images des Mathématiques Certifiées ?

La journée a été filmée, les vidéos devraient bientôt être disponibles sur le site de l’IHP.