Programmer des démonstrations : une modeste invitation aux assistants de preuve

Posté par  (site web personnel, Mastodon) . Édité par Benoît Sibaud et cli345. Modéré par Benoît Sibaud. Licence CC By‑SA.
Étiquettes :
47
24
fév.
2025
Science

En principe, une démonstration mathématique ne fait que suivre des règles logiques bien définies, et devrait donc pouvoir être encodée informatiquement et vérifiée par un ordinateur. Où en est-on dans la pratique et dans la théorie ? Petit tour au pays des assistants de preuve, des langages de programmation dédiés aux démonstrations, et de leur fondement théorique le plus commun, la théorie des types.

Sommaire

Vérifier des programmes

Comme nous sommes sur LinuxFr.org, je devrais peut-être commencer par ceci : nous passons énormément de temps à découvrir des bugs, et pour les personnes du développement logiciel, à les comprendre, à les résoudre, et de préférence à les éviter en écrivant des tests.

Dans une formation universitaire de base en informatique, on rencontre des algorithmes, mais aussi des méthodes pour prouver que ces algorithmes terminent et répondent bien au problème posé. Les premières introduites sont typiquement les variants de boucle (montrer qu’une certaine valeur décroît à chaque itération, ce qui assure que le programme termine si elle ne peut pas décroître à l’infini), et les invariants de boucle (montrer qu’une certaine propriété vraie au début d’une boucle est préservée entre deux itérations, ce qui assure qu’elle reste encore vraie à la fin de la boucle).

On a donc, d’une part, un algorithme, implémentable sur machine, d’autre part une preuve, sur papier, que l’algorithme est correct. Mais si l’implémentation a une erreur par rapport à l’algorithme sur papier ? Et puisque nous n’arrêtons pas de nous tromper dans nos programmes, il est fort possible que nous nous trompions dans notre preuve (qui n’a jamais oublié qu’il fallait faire quelque chose de spécial dans le cas n = 0 ?).

En tant que programmeurs, on peut imaginer une approche où non seulement l’algorithme est implémenté, mais sa preuve de terminaison et de correction est aussi « implémentée », c’est-à-dire encodée dans un langage qui ressemble à un langage de programmation, pour être ensuite non pas interprétée ou compilée mais vérifiée.

La vérification est un très vaste domaine de l’informatique, dont je ne suis pas spécialiste du tout, et dans lequel il existe énormément d’approches : la logique de Hoare (voir par exemple l’outil why3), qui est essentiellement un raffinement des variants et invariants de boucle, la logique de séparation spécialement conçue pour raisonner sur la mémoire mutable (voir Iris), le model checking qui se concentre sur des programmes d’une forme particulièrement simple (typiquement des systèmes de transition finis) pour en vérifier des propriétés de façon complètement automatisée, etc.

Dans cette dépêche, je vais parler d’une approche avec quelques caractéristiques particulières :

  • On vérifie des programmes purement fonctionnels (pas d’effets de bord, même si on peut les simuler).

  • Le même langage mélange à la fois les programmes et leurs preuves.

  • Plus précisément, le langage ne fait pas (ou peu) de distinction entre les programmes et les preuves.

Vérifier des démonstrations mathématiques

Pour se convaincre de l’ampleur que les démonstrations ont prise dans les mathématiques contemporaines, il suffit d’aller jeter un œil, par exemple, au projet Stacks : un livre de référence sur la géométrie algébrique, écrit collaborativement sur les 20 dernières années, dont l’intégrale totalise plus de 7500 pages très techniques. Ou bien la démonstration du théorème de classification des groupes finis simples : la combinaison de résultats répartis dans les dizaines de milliers de pages de centaines d’articles, et une preuve « simplifiée » toujours en train d’être écrite et qui devrait faire plus de 5000 pages. Ou bien le théorème de Robertson-Seymour, monument de la théorie des graphes aux nombreuses applications algorithmiques : 20 articles publiés sur 20 ans, 400 pages en tout. Ou bien, tout simplement, le nombre de références dans la bibliographie de la moindre thèse ou d’articles publiés récemment sur arXiv.

Inévitablement, beaucoup de ces démonstrations contiennent des erreurs. Parfois découvertes, parfois beaucoup plus tard. Un exemple assez célèbre est celui d’un théorème, qui aurait été très important s’il avait été vrai, publié en 1989 par Vladimir Voedvodsky, un célèbre mathématicien dont je vais être amené à reparler plus bas, avec Mikhail Kapranov. Comme raconté par Voedvodsky lui-même, un contre-exemple a été proposé par Carlos Simpson en 1998, mais jusqu’en 2013, Voedvodsky lui-même n’était pas sûr duquel était faux entre sa preuve et le contre-exemple !

Il y a aussi, souvent, des « trous », qui ne mettent pas tant en danger la démonstration mais restent gênants : par exemple, « il est clair que la méthode classique de compactification des espaces Lindelöf s’applique aussi aux espaces quasi-Lindelöf », quand l’auteur pense évident qu’un argument existant s’adapte au cas dont il a besoin mais que ce serait trop de travail de le rédiger entièrement. Donc, assez naturellement, un but possible de la formalisation des maths est de produire des démonstrations qui soient certifiées sans erreur (et sans trou).

Mais c’est loin d’être le seul argument. On peut espérer d’autres avantages, qui pour l’instant restent de la science-fiction, mais après tout ce n’est que le début : par exemple, on peut imaginer que des collaborations à grande échelle entre beaucoup de mathématiciens deviennent possibles, grâce au fait qu’il est beaucoup plus facile de réutiliser le travail partiel de quelqu’un d’autre s’il est formalisé que s’il est donné sous formes d’ébauches informelles pas complètement rédigées.

Brouwer-Heyting-Kolmogorov

Parmi les assistants de preuve existants, la plupart (mais pas tous) se fondent sur une famille de systèmes logiques rangés dans la famille des « théories des types ». L’une des raisons pour lesquelles ces systèmes sont assez naturels pour être utilisés en pratique est qu’en théorie des types, les preuves et les programmes deviennent entièrement confondus ou presque, ce qui rend facile le mélange entre les deux.

Mais comment est-ce qu’un programme devient une preuve, au juste ? L’idée de base est appelée interprétation de Brouwer-Heyting-Kolomogorov et veut que les preuves mathématiques se comprennent de la façon suivante :

  • Le moyen de base pour prouver une proposition de la forme « P et Q » est de fournir d’une part une preuve de P et une preuve de Q. En d’autres mots, une preuve de « P et Q » rassemble en un même objet une preuve de P et une preuve de Q. Mais en termes informatiques, ceci signifie qu’une preuve de « P et Q » est une paire d’une preuve de P et d’une preuve de Q.

  • De même, pour prouver « P ou Q », on peut prouver P, ou on peut prouver Q. Informatiquement, une preuve de « P ou Q » va être une union disjointe : une preuve de P ou une preuve de Q, avec un bit pour savoir dans quel cas on est.

  • Pour prouver « Vrai », il suffit de dire « c’est vrai » : on a une unique preuve de « Vrai ».

  • On ne doit pas pouvoir prouver « Faux », donc une preuve de « Faux » n’existe pas.

  • Et le plus intéressant : pour prouver « si P alors Q », on suppose temporairement P et on en déduit Q. Informatiquement, ceci doit devenir une fonction qui prend une preuve de P et renvoie une preuve de Q.

Curry-Howard

L’interprétation de Brouwer-Heyting-Kolmogorov est informelle, et il existe plusieurs manières de la rendre formelle. Par exemple, on peut interpréter tout ceci par des programmes dans un langage complètement non-typé, ce qui s’appelle la réalisabilité.

Mais en théorie des types, on prend plutôt un langage statiquement typé pour suivre l’idée suivante : si une preuve de P et Q est une paire d’une preuve de P et d’une preuve de Q, alors le type des paires de P et Q peut se comprendre comme le type des preuves de « P et Q ». On peut faire de même avec les autres types de preuves, et ceci s’appelle la correspondance de Curry-Howard. Autrement dit, là où Brouwer-Heyting-Kolmogorov est une correspondance entre les preuves et les programmes, Curry-Howard est un raffinement qui met aussi en correspondance les propositions logiques avec les types du langage, et la vérification des preuves se confond entièrement avec le type checking.

Sur les cas que j’ai donnés, la correspondance de Curry-Howard donne :

  • La proposition « P et Q » est le type des paires d’un élément de P et d’un élément de Q,

  • La proposition « P ou Q » est le type somme de P et Q (comme Either en Haskell et OCaml, les tagged unions en C, et std::variant en C++ : l’un ou l’autre, avec un booléen pour savoir lequel),

  • La proposition « Vrai » est le type trivial à une seule valeur (comme () en Haskell et Rust, unit en OCaml),

  • La proposition « Faux » est le type vide qui n’a aucune valeur (comme ! en Rust),

  • La proposition « si P alors Q » est le type des fonctions qui prennent un argument de type P et renvoient une valeur de type Q.

Quantificateurs et types dépendants

La version de Curry-Howard que j’ai esquissée donne une logique dite « propositionnelle » : il n’y a que des propositions, avec des connecteurs entre elles. Mais en maths, on ne parle évidemment pas que des propositions. On parle de nombres, de structures algébriques, d’espaces topologiques, …, bref, d’objets mathématiques, et des propriétés de ces objets. Les deux types principaux de propositions qui manquent sont ce qu’on appelle les quantificateurs : « Pour tout x, … » et « Il existe x tel que… ». Ici, ce qui est une évidence en logique devient moins évident, mais très intéressant, du côté des programmes.

Prenons pour l’exemple le théorème des deux carrés de Fermat, qui énonce (dans l’une de ses variantes) qu’un nombre premier impair est de la forme 4n+1 si et seulement s’il peut s’écrire comme somme de deux carrés parfaits. À quoi doit ressembler le type associé à cette proposition ? Par analogie avec les implications, on a envie de dire que cela devrait être une fonction, qui prend un nombre premier impair p, et renvoie une preuve de l’équivalence. Problème : ce qui est à droite de l’équivalence est une proposition paramétrée par p. Autrement dit, en notant P le type des nombres premiers impairs, on ne veut plus un simple type fonction P → E, mais un type fonction où le type de retour peut dépendre de la valeur passée à la fonction, noté par exemple (p : P) → E(p). Ces types qui dépendent de valeurs sont appelés types dépendants.

Dans les langages de programmation populaires, il est rare de trouver des types dépendants. Mais on en retrouve une forme faible en C avec les tableaux de longueur variable (VLA pour « variable-length arrays ») : on peut écrire

… f(int n) {
  int array[n];
  …
}

qui déclare un tableau dont la taille n est une expression. Néanmoins, en C, même si on dispose de ce type tableau qui est en quelque sorte dépendant, on ne peut pas écrire une fonction « int[n] f(int n) » qui renvoie un tableau dont la longueur est passée en paramètre. Plus récemment, en Rust, il existe les const generics, où des valeurs se retrouvent dans les types et où on peut écrire fn f<const n: usize>() -> [u8; n], ce qui est un vrai type dépendant, mais cette fois avec la restriction assez sévère que toutes ces valeurs peuvent être calculées entièrement à la compilation, ce qui à cause de la façon dont fonctionne ce type de calcul en Rust empêche par exemple les allocations mémoire. (Donc l’implémentation est assez différente, elle efface ces valeurs en « monomorphisant » tous les endroits où elles apparaissent.)

En théorie des types, le langage est (normalement) purement fonctionnel, donc les problèmes d’effets de bord dans les valeurs à l’intérieur des types dépendants ne se pose pas. Le type checking peut déclencher des calculs arbitrairement complexes pour calculer les valeurs qui se trouvent dans les types.

Et le « il existe », au fait, à quoi correspond-il ? Cette fois, ce n’est plus une fonction dépendante mais une paire dépendante : une preuve de « Il existe x tel que E(x) » est une paire d’une valeur x et d’une preuve de E(x). La différence avec une paire normale est que le type du deuxième élément peut dépendre de la valeur du premier élément.

Comme on peut commencer à s’en douter, le fait d’avoir des types dépendants est utile pour prouver des affirmations mathématiques, mais aussi, bien qu’il puisse sembler inhabituel, pour prouver des programmes, et plus précisément pour encoder des propriétés des valeurs dans les types. Là où on aurait dans un langage moins expressif une fonction qui renvoie deux listes, avec une remarque dans la documentation qu’elles sont toujours de même taille, dans un langage avec des types dépendants, on peut renvoyer un triplet d’un entier n, d’une liste dont le type indique qu’elle est de taille n, et une deuxième liste elle aussi de taille n. Et là où on aurait un deuxieme_liste[indice_venant_de_la_premiere] avec un commentaire que cela ne peut pas produire d’erreur, car les deux listes sont de même taille, on a un programme qui utilise la garantie que les deux listes sont de même taille, et le typage garantit statiquement que cette opération t[i] ne produira pas d’erreur.

Logique intuitionniste

Reprenons l’exemple du théorème des deux carrés de Fermat. Nous pouvons maintenant traduire cette proposition en un type : celui des fonctions qui prennent un nombre premier impair p et renvoient une paire de :

  • Une fonction qui prend n tel que p = 4n+1 et renvoie deux entiers a, b accompagnés d’une preuve que a^2 + b^2 = p,

  • Réciproquement, une fonction qui prend a, b et une preuve de a^2 + b^2 = p, et renvoie n tel que p = 4n+1.

Prouver le théorème des deux carrés de Fermat en théorie des types, c’est donner un élément (on dit plutôt « habitant ») de ce type, soit un programme dont le langage peut vérifier qu’il a ce type. Mais que fait au juste ce programme quand on l’exécute ? On voit qu’il permet notamment de calculer une décomposition d’un nombre premier impair congru à 1 modulo 4 comme somme de deux carrés.

Là, c’est le côté « programmes » qui apporte un élément moins habituel du côté « preuves » : l’exécution d’un programme va correspondre à un processus de simplification des preuves. Notamment, si on a une preuve de « si P alors Q » et une preuve de P, on peut prendre la preuve de P et remplacer chaque utilisation de l’hypothèse P dans la preuve de « si P alors Q », pour obtenir une preuve de Q qui peut contenir de multiples copies d’une même preuve de P. Cette opération de simplification du côté logique correspond naturellement au fait que la manière en théorie des types de prouver Q à partir d’une preuve f de P ⇒ Q et d’une preuve x de P est tout simplement d’écrire f(x), et que calculer f(x), informatiquement, se fait bien en remplaçant le paramètre de f à tous les endroits où il apparaît par la valeur x et à simplifier le résultat. On dit que la logique de Curry-Howard est constructive, parce qu’elle se prête à une interprétation algorithmique.

Mais ceci peut sembler gênant. Par exemple, il est trivial en maths « normales » de prouver que tout programme termine ou ne termine pas. Mais par Curry-Howard, une preuve que tout programme termine ou ne termine pas doit être une fonction qui prend un programme, et qui renvoie soit une preuve qu’il termine, soit une preuve qu’il ne termine pas. Autrement dit, si cette proposition censément triviale était prouvable dans Curry-Howard, on aurait un algorithme pour résoudre le problème de l’arrêt, ce qui est bien connu pour être impossible.

L’explication à cette différence tient au fait que la preuve « triviale » de cette proposition utilise une règle de déduction qui a un statut un peu à part en logique, dite règle du tiers exclu : pour n’importe quelle proposition P, sans aucune hypothèse, on peut déduire « P ou (non P) » (autrement dit, que P est vraie ou fausse). Or cette règle n’admet pas d’interprétation évidente par Curry-Howard : le tiers exclu devrait prendre une proposition P et renvoyer soit une preuve de P, soit une preuve que P est fausse (ce qui s’encode par « si P alors Faux »), autrement dit, le tiers exclu devrait être un oracle omniscient capable de vous dire si une proposition arbitraire est vraie ou fausse, et ceci est bien évidemment impossible.

(Cela dit, si vous voulez vous faire mal à la tête, apprenez que c’est l’opérateur call/cc et pourquoi l’ajouter permet de prouver le tiers exclu. Exercice : call/cc existe dans de vrais langages, comme Scheme, pourtant on vient de voir que le tiers exclu semble nécessiter un oracle omniscient, comment expliquer cela ?)

Pour être précis, la logique sans le tiers exclu est dite intuitionniste (le terme constructive étant un peu flou, alors que celui-ci est précis). On peut faire des maths en restant entièrement en logique intuitionniste, et même si ce n’est pas le cas de l’écrasante majorité des maths, il existe tout de même un certain nombre de chercheurs qui le font, et ceci peut avoir divers intérêts. Il y a notamment l’interprétation algorithmique des théorèmes, mais aussi, de manière beaucoup plus avancée, le fait que certaines structures mathématiques (topos, ∞-topos et consorts) peuvent s’interpréter comme des sortes d’univers mathématiques alternatifs régis par les règles de la logique intuitionniste (techniquement, des « modèles » de cette logique), et que parfois il est plus simple de prouver un théorème en le traduisant à l’intérieur de l’univers et en prouvant cette version traduite de manière intuitionniste.

Pour pouvoir malgré tout raisonner en théorie des types de manière classique (par opposition à intuitionniste), il suffit de postuler le tiers exclu comme axiome. Du point de vue des programmes, cela revient à rajouter une constante qui est supposée avoir un certain type mais qui n’a pas de définition (cela peut donc rendre les programmes impossibles à exécuter, ce qui est normal pour le tiers exclu).

Quelques exemples

Si vous aviez décroché, c’est le moment de reprendre. Parlons un peu des assistants de preuve qui existent. Les plus connus sont :

  • Rocq, anciennement nommé Coq, développé à l’Inria depuis 1989, écrit en OCaml, sous licence LGPL 2.1. Il est assez lié à l’histoire de la théorie des types, car il a été créé par Thierry Coquand comme première implémentation du calcul des constructions, une théorie des types inventée par Coquand et devenue l’une des principales existantes. (Oui, Coq a été renommé en Rocq à cause de l’homophonie en anglais entre « Coq » et « cock ». J’apprécierais que les commentaires ne se transforment pas en flame war sur ce sujet très peu intéressant, merci.)

  • Lean, créé par Leonardo de Moura et développé depuis 2013 lorsqu'il était chez Microsoft Research, écrit initialement en C++ et désormais en Lean, placé sous licence Apache 2.0.

  • Agda, créé par Ulf Norrell en 1999, écrit en Haskell et sous licence BSD 1-clause.

  • D’autres que je connais moins, notamment Isabelle et F* (liste sur Wikipédia).

Pour illustrer comment peuvent fonctionner les choses en pratique, voici un exemple très simple de code en Agda :

open import Agda.Primitive using (Level)
open import Data.Product using (_×_; _,_)

swap : {ℓ₁ ℓ₂ : Level}  {P : Set ℓ₁} {Q : Set ℓ₂}  P × Q  Q × P
swap (p , q) = (q , p)

Vue comme un programme, cette fonction swap inverse simplement les deux éléments d’une paire. Vue comme une preuve, elle montre que pour toutes propositions P et Q, si P et Q, alors Q et P. Comme le veut Curry-Howard, les deux ne sont pas distingués. Les types P et Q sont eux-mêmes dans des types \mathsf{Set}_\ell avec un « niveau » \ell, ceci parce que, pour des raisons logiques, il serait incohérent que le type des types soit de son propre type, donc on a un premier type de types \mathsf{Set}_0, qui est lui-même de type \mathsf{Set}_1, et ainsi de suite avec une hiérarchie infinie de niveaux appelés univers. À un niveau plus superficiel, on remarquera qu’Agda a une syntaxe qui ressemble fort à Haskell (et utilise intensivement Unicode).

Voilà la même chose en Rocq :

Definition swap {P Q : Prop} : P /\ Q -> Q /\ P :=
  fun H => match H with conj p q => conj q p end.

La syntaxe est assez différente et ressemble plutôt à OCaml (normal, vu que Rocq est écrit en OCaml et Agda en Haskell). Mais à un niveau plus profond, on voit apparaître un type Prop dont le nom évoque furieusement les propositions. Or j’avais promis que les propositions seraient confondues avec les types, donc pourquoi a-t-on un type spécial pour les propositions ?

En réalité, pour diverses raisons, il peut être intéressant de briser l’analogie d’origine de Curry-Howard et de séparer les propositions et les autres types en deux mondes qui se comportent de façon extrêmement similaire mais restent néanmoins distincts. Notamment, un principe qu’on applique sans réfléchir en maths est que si deux propositions sont équivalentes, alors elles sont égales (extensionnalité propositionnelle), mais on ne veut clairement pas ceci pour tous les types (on peut donner des fonctions bool -> int et int -> bool, pourtant on ne veut certainement pas bool = int), donc séparer les propositions des autres permet d’ajouter l’extensionnalité propositionnelle comme axiome. (Mais il y a aussi des différences comme l'imprédicativité dans lesquelles je ne vais pas rentrer.)

Et voici encore le même code, cette fois en Lean :

def swap {P Q : Prop} : P  Q  Q  P :=
  fun p, q => q, p

À part les différences de syntaxe, c’est très similaire à Rocq, parce que Lean a aussi une séparation entre les propositions et les autres types.

Cependant, en Rocq et Lean, on peut aussi prouver la même proposition de façon différente :

Lemma swap {P Q : Prop} : P /\ Q -> Q /\ P.
Proof.
  intros H. destruct H as [p q]. split.
  - apply q.
  - apply p.
Qed.

et

def swap {P Q : Prop} : P  Q  Q  P := by
  intro h
  have p := h.left
  have q := h.right
  exact q, p

Avec Proof. ou by, on entre dans un mode où les preuves ne sont plus écrites à la main comme programmes, mais avec des tactiques, qui génèrent des programmes. Il existe toutes sortes de tactiques, pour appliquer des théorèmes existants, raisonner par récurrence, résoudre des inégalités, ou même effectuer de la recherche automatique de démonstration, ce qui s’avère extrêmement utile pour simplifier les preuves.

Ce mode « tactiques » permet aussi d’écrire la preuve de façon incrémentale, en faisant un point d’étape après chaque tactique pour voir ce qui est prouvé et ce qui reste à prouver. Voici par exemple ce qu’affiche Rocq après le destruct et avant le split :

  P, Q : Prop
  p : P
  q : Q
  ============================
  Q /\ P

Cette notation signifie que le contexte ambiant contient les variables P et Q de type Prop ainsi que p une preuve de P (donc un élément du type P) et q une preuve de Q. Le Q /\ P en dessous de la barre horizontale est le but à prouver, c’est-à-dire le type dont on cherche à construire un élément.

Agda fonctionne assez différemment : il n’y a pas de tactiques, mais il existe néanmoins un système de méta-programmation qui sert à faire de la recherche de preuves (donc contrairement à Rocq et Lean, on n’écrit pas la majeure partie des preuves avec des tactiques, mais on peut se servir d’un équivalent quand c’est utile). Pour écrire les preuves incrémentalement, on met ? dans le programme quand on veut ouvrir une sous-preuve, et Agda va faire le type-checking de tout le reste et donner le contexte à l’endroit du ?.

Quelques succès de la formalisation

En 2025, la formalisation reste très fastidieuse, mais elle a déjà eu plusieurs grands succès :

Actuellement, Lean a réussi à attirer une communauté de mathématiciens qui développent mathlib (1,1 million de lignes de code Lean au moment où j’écris), une bibliothèque de définitions et théorèmes mathématiques qui vise à être la plus unifiée possible.

Les équivalents dans d’autres assistants de preuve se développent même s’ils ne sont pas (encore) aussi gros : citons mathcomp, unimath, agda-unimath entre autres.

Un autre grand succès, dans le domaine de la vérification cette fois, est CompCert (malheureusement non-libre), qui est un compilateur C entièrement écrit en Rocq et vérifié par rapport à une spécification du C également encodée en Rocq.

La recherche en théorie des types

La théorie des types est un domaine de recherche à part entière, qui vise à étudier du point de vue logique les théories des types existantes, et à en développer de nouvelles pour des raisons à la fois théoriques et pratiques.

Historiquement, une grande question de la théorie des types est celle de comprendre à quel type doivent correspondre les propositions d’égalité. Par exemple, on veut que deux propositions équivalentes soient égales, et que deux fonctions qui prennent les mêmes valeurs soient égales, et éventuellement pour diverses raisons que deux preuves de la même proposition soient égales, mais s’il est facile d’ajouter toutes ces choses comme axiomes, il est très compliqué de les rendre prouvables sans obtenir, comme avec le tiers exclu, des programmes qui ne peuvent pas s’exécuter à cause des axiomes qui sont déclarés sans définition.

Vladimir Voedvodsky a fait une contribution majeure en proposant un nouvel axiome, appelé univalence, qui dit très sommairement que si deux types ont la même structure (on peut donner une « équivalence » entre les deux), alors ils sont en fait égaux (résumé simpliste à ne pas prendre au mot). Cet axiome est très pratique pour faire des maths parce qu’on travaille souvent avec des objets qui ont la même structure (on dit qu’ils sont isomorphes), et qui doivent donc avoir les mêmes propriétés, et cet axiome permet de les identifier (même s’il a aussi des conséquences qui peuvent paraître choquantes). Sa proposition a donné naissance à une branche appelée théorie homotopique des types, qui explore les maths avec univalence. Le prix à payer est que les types ne se comprennent plus comme de simples ensembles de valeurs (ou de preuves d’une proposition), mais comme des espaces géométriques munis de toute une structure complexe (techniquement, les égalités sont des chemins entre points, et il y a des égalités non-triviales, des égalités entre égalités, etc.), et la compréhension de ces espaces-types est fondée sur la théorie de l’homotopie. Il y a bien d’autres théories des types, avec univalence ou non : théorie cubique des types, théorie des types observationnelle, etc.

Conclusion

J’espère avoir communiqué un peu de mon enthousiasme pour le domaine (dans lequel je suis probablement parti pour démarrer une thèse). Si vous voulez apprendre un assistant de preuve, une ressource assez abordable est la série Software Foundations avec Rocq. Il existe également Theorem proving in Lean 4 et divers tutoriels Agda. Vous pouvez aussi essayer ces assistants de preuve directement dans votre navigateur : Rocq, Lean ou Agda. Et bien sûr les installer et jouer avec : Rocq, Lean, Agda.

Aller plus loin

  • # Merci

    Posté par  . Évalué à 2 (+2/-0).

    Merci pour cet article.
    C'est un sujet que je connais peu, bien qu'ayant fait des études en mathématiques (appliquées).
    Bon courage pour la thèse ! :)

  • # Reproductibilité, vérifiabilité et musiciens de Brême

    Posté par  (site web personnel) . Évalué à 5 (+2/-0).

    J'aime bien le grand écart entre ces tendances plus ou moins antagonistes : le code que l'on veut prouver et qui doit faire exactement ce qui est attendu, la compilation qui doit être totalement reproductible bit à bit pour faire exactement ce qui est attendu, et l'intelligence artificielle qui doit faire quelque chose, potentiellement ce qui est attendu et de façon pas forcément comprise ou explicable (même si des personnes travaillent d'ores et déjà sur de l'« IA explicable »).

    (et anecdotiquement ça me fait penser aux musiciens de Brême parce qu'on a déjà le (R)coq, le chat(GPT)… reste à trouver le chien et l'âne - et je vous vois venir)

    • [^] # Re: Reproductibilité, vérifiabilité et musiciens de Brême

      Posté par  (site web personnel, Mastodon) . Évalué à 3 (+0/-0).

      Merci (?) de m'avoir remis dans la tête l'air "Les musiciens de Brême, hihan, han han" tiré d'un livre-disques basé sur le conte et que mes petits frères écoutaient en boucle. (je sais ça pourrait être pire).

      « Tak ne veut pas quʼon pense à lui, il veut quʼon pense », Terry Pratchett, Déraillé.

    • [^] # Re: Reproductibilité, vérifiabilité et musiciens de Brême

      Posté par  . Évalué à 2 (+0/-0).

      J'aime bien le grand écart entre ces tendances plus ou moins antagonistes

      Ces tendances ne sont pas antagonistes et peuvent parfaitement coopérer. Ce qui m'a gêné dernièrement, c'est plus ceux qui s'emballent sur les succès récents de la technologie des LLM. Mais combiner des LLM avec des méthodes formelles comme la vérification ou la recherche automatique de preuves, cela se fait : Imandra, par exemple.

      Sur l'emballement au sujet des LLM et des machines soit disant intelligentes, cela me rappelle une anecdote. Il y a 20 ans, ma compagne de l'époque était journaliste et utilisait du speech-to-text (algorithmique que l'on retrouve dans l'apprentissage automatique) pour l'aider à retranscrire ses interviews enregistrés sur dictaphone.. Un jour j'essaye de lui expliquer que l'on peut programmer un ordinateur pour qu'il est 20 au bac S en maths (on sait faire ça depuis longtemps via les approches formelles) : elle n'a jamais voulu me croire ! Une machine ne pouvait pas être aussi « intelligente » pour elle (le fait qu'elle utilise du speech-to-text me faisait rire intérieurement ;-). Je me demande bien ce qu'elle pense aujourd'hui d'un logiciel comme ChatGPT.

      Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

  • # Merci

    Posté par  . Évalué à 4 (+3/-0).

    Merci pour ce travail de communication très intéressant !

  • # Pour la complétude, j'ajoute le couple SPARK/Ada

    Posté par  (site web personnel) . Évalué à 3 (+2/-0).

    Ca ne va pas compléter la pyramide animale des musiciens de Brême, ni contribuer à ce très intéressant état de l'art mathématique sur le sujet, mais pour l'anecdote j'ajoute l'exemple de la spécification de la procedure Swap avec le prouveur SPARK et le langage Ada :

        procedure Swap (A, B : in out Integer)
           with Post => A = B'Old and B = A'Old;

    Intéressant au passage de voir comment la syntaxe des langages, en utilisant plus ou moins de symboles, se destine plus à des mathématiciens ou à des béotiens informaticiens.

    PS1 : je ne fais pas partie des spécialistes de SPARK
    PS2 : je fais partie des béotiens :-)

    • [^] # Re: Pour la complétude, j'ajoute le couple SPARK/Ada

      Posté par  . Évalué à 4 (+1/-0).

      C'est pas tout à fait le même niveau de généralité non ? Ici tu fixes un type pour A et B, Integer, on a au moins besoin de paramétrer la procédure, A et B sont dans les autres exemples des variables de types qu'on doit préciser lors de l'appel à la procédure.

      • [^] # Re: Pour la complétude, j'ajoute le couple SPARK/Ada

        Posté par  (site web personnel, Mastodon) . Évalué à 3 (+1/-0).

        Oui, voilà, ça m'a l'air d'être de la logique de Hoare, pas de la théorie des types.

        • [^] # Re: Pour la complétude, j'ajoute le couple SPARK/Ada

          Posté par  (site web personnel) . Évalué à 1 (+0/-0).

          Et voilà, quand on fait des commentaires en béotien, on tombe à côté :-)

          Ce n'est probablement pas lié à la définition de SPARK himself, mais je crois que gnatprove utilise Why3.
          Je ne comprends pas ce que cela implique, mais comme tu l'as associé à la logique de Hoare dans ton intro, ça semble confirmer.

        • [^] # Re: Pour la complétude, j'ajoute le couple SPARK/Ada

          Posté par  . Évalué à 3 (+1/-0).

          Le langage fonctionnant par effet de bords, il faut effectivement utiliser la logique de Hoare pour vérifier la correction des programmes écrits avec.

          Cela étant, il me semble que Thomas voulait dire que l'exemple était monomorphe (les deux variables d'entrées sont de types Int) et non polymorphes (il n'y a pas de variable de types); d'où sa remarque sur le manque de généralité.

          Quoi qu'il en soit, la logique de Hoare est une proche parente de la théorie des types en partageant le même fondement : la structure logico-déductive de l'ésprit humain. Par exemple, la règle de composition :

          {P} S {Q} , {Q} T {R}
          ---------------------
              {P} S; T {R}
          

          est la version impérative du typage de la composition de fonction dans les langages fonctionnels (('p -> 'q) -> ('q -> 'r) -> 'p -> 'r dans le langage des types de OCaml), règle qui a pour fondement une double application du modus ponens (si A alors B, or A, donc B).

          Les programmeurs impératifs composent les instructions, comme les programmeurs fonctionnels composent les fonctions.

          P.S : Joli dépêche qui résume bien le domaine et l'état des lieux. J'étais passé à côté et je compte bien t'écrire un commentaire plus long et détaillé (qui me demandera plus de temps que cette simple remarque sur la logique de Haore). En plus, ça me permettra de parler de mes marottes (la logique formelle, la théorie de la démonstration, la correspondance de Curry-Howard et la philosophie des mathématiques) sans que thoasm m'en fasse le reproche. ;-)

          Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

  • # Clichés

    Posté par  (site web personnel) . Évalué à 4 (+4/-1).

    Comme nous sommes sur LinuxFr.org, je devrais peut-être commencer par ceci : tous, nous passons énormément de temps à découvrir des bugs, à les comprendre, à les résoudre, et de préférence à les éviter en écrivant des tests.

    Il semble certes y avoir beaucoup de développeurs à commenter sur DLFP, m'enfin cette généralisation me semble abusive, limite insultante

    • [^] # Re: Clichés

      Posté par  (site web personnel, Mastodon) . Évalué à 4 (+2/-0).

      Je ne suis pas développeur moi-même, pourtant je certifie que je passe énormément de temps à découvrir des bugs dans l'intranet de mon école, dans mon émulateur de terminal, dans Firefox, … 🙂 Certes, ce n'est pas moi qui écris les tests. Mais si un modérateur passe par là, on pourrait effectivement changer ça en « tous les développeurs (voire les autres !) passent … »

    • [^] # Re: Clichés

      Posté par  (site web personnel) . Évalué à 3 (+1/-0).

      C'est vrai. Un développeur sachant développer doit savoir écrire des bugs sans les découvrir par lui-même. :)

      Adhérer à l'April, ça vous tente ?

      • [^] # Re: Clichés

        Posté par  . Évalué à 3 (+0/-0).

        Y a-t-il un développeur qui soit capable de trouver tous les bugs ? Est-il compris dans l'ensemble des développeurs capables de se corriger eux même ? Quid des bugs créés par des non développeurs ? Est-il un non développeur lui même ?

        pars chercher un comprimé de paracétamol

    • [^] # Re: Clichés

      Posté par  (site web personnel) . Évalué à 1 (+0/-0).

      Très bien merci ! Le reste de l'article n'est pas tellement plus digeste pour autant :-D

  • # Petite rectification

    Posté par  (site web personnel, Mastodon) . Évalué à 2 (+0/-0).

    Comme me l'a fait remarquer Patrick Massot, la ligne

    Lean, créé par Leonardo de Moura et développé depuis 2013 chez Microsoft Research, écrit en C++, placé sous licence Apache 2.0.

    contient des infos obsolètes : Leonardo de Moura ne travaille plus chez Microsoft Research, et contrairement à Lean 3, Lean 4 est principalement écrit en Lean 4 (je n'ai pas regardé comment c'était bootstrappé).

    Est-ce qu'un modérateur voudrait bien corriger ça ? Merci !

    • [^] # Re: Petite rectification

      Posté par  (site web personnel) . Évalué à 3 (+0/-0).

      Corrigé, merci.

    • [^] # Re: Petite rectification

      Posté par  (site web personnel, Mastodon) . Évalué à 2 (+0/-0).

      Pourtant la citation ne me semble pas fausse (:
      - il l’a créé et ce fait ne peut pas devenir obsolète…
      - c’est toujours développé/maintenu par la firme de Redmond et il n’était pas dit que le créateur y travaillait ou y travaille encore…
      - que la dernière version ne soit plus écrite en C++ n'invalide pas le fait que ça l’était au début…

      Je suis bien d’accord qu’il faut clarifier, juste qu’il ne faut pas conclure que les infos étaient obsolètes (en tout cas moi j’avais bien lu comme un « historique » la première fois, et non des faits actuels, ce qui peut être un biais je le conçois.)

      “It is seldom that liberty of any kind is lost all at once.” ― David Hume

  • # Lean vs Rock

    Posté par  (site web personnel, Mastodon) . Évalué à 2 (+1/-0).

    Rock était bien établi et complet et maintenant Lean , le petit nouveau, semble dominer. Y a t’il une raison à cela?
    Je veux dire on ne crée pas un nouveau langage pour le plaisir mais pour apporter quelque chose en plus. Et en plus à priori Lean est similaire à Rock.

    Sous licence Creative common. Lisez, copiez, modifiez faites en ce que vous voulez.

    • [^] # Re: Lean vs Rock

      Posté par  (site web personnel, Mastodon) . Évalué à 4 (+2/-0).

      Lean est dominant dans le domaine de la formalisation des maths, mais Agda avance pas mal aussi, et largement dans une autre direction puisque la plupart des gens qui font de la théorie homotopique des types (dans l'une de ses variantes, p.ex. la théorie cubique des types) le font en Agda (certains le font en Rocq aussi, mais Lean ne le permet pas du tout). Et j'ai l'impression que Rocq reste le plus utilisé pour la vérification de programmes, mais c'est peut-être mon biais d'observation qui fait ça (parce que je suis plus au contact de la recherche qui se fait en France, et Rocq est développé par l'Inria et beaucoup utilisé dans les labos français) ; en tous cas c'est sûr que CompCert et Iris, des outils assez connus, sont construits sur Rocq.

      Quoi qu'il en soit, je pense qu'il ne faut pas le voir comme un concours : c'est une bonne chose qu'il y a plusieurs outils en parallèle, parce que ça leur fait explorer des pistes différentes, ça évite le lock-in exclusif à un outil qui empêche l'innovation ensuite, etc.

      Quelques différences entre Rocq et Lean :

      • Lean a une grosse particularité dans sa théorie des types, qui s'appelle la « proof irrelevance définitionnelle », et qui peut être très pratique mais a aussi pour conséquence de casser plein de bonnes propriétés théoriques de la théorie des types. Notamment, le type checking de Lean est une approximation d'un problème indécidable, et contrairement à presque toutes les théories de types, il existe en fait des programmes qui ne terminent pas (des termes non fortement normalisables). Rocq a fini par introduire cette particularité sous une forme plus faible qui n'a pas ces conséquences désagréables, mais pour garder la compatibilité avec l'existant, ils l'ont fait avec un autre univers de propositions, du coup on a deux univers, SProp et Prop, qui coexistent, et SProp n'est pas très agréable en pratique parce que toutes les librairies existantes sont écrites avec Prop.

      • Globalement, il y a plus de vieilleries dans Rocq, c'est un peu normal vu son âge. Il y a plein de fonctionnalités qui font des choses similaires mais pas tout à fait identiques, souvent pour des raisons de compatibilité. (Ltac vs Ltac2 vs Mtac, tactiques standard vs SSreflect, inductifs simples vs records, classes de type vs instances canoniques, #[refine] vs Program, etc.) De plus la bibliothèque standard de Lean est vraiment beaucoup mieux faite. C'est subjectif mais je pense que la plupart des gens seront d'accord pour dire que Lean est mieux ingéniéré et a tiré des leçons de certains aspects moins bien faits de Rocq.

      • Comme il s'adresse largement à des matheux qui n'y connaissent rien à la logique intuitionniste, Lean n'a pas peur d'utiliser le tiers exclu, et aussi d'autres axiomes comme l'extensionnalité fonctionnelle, l'extensionnalité propositionnelle, les types quotients et l'axiome du choix. Ça n'empêche pas de raisonner sans ces axiomes en Lean, mais c'est lourdingue parce que toutes les tactiques standard les introduisent même quand elles n'en auraient pas besoin.

      • Rocq, en plus de permettre de faire de la théorie homotopique des types, a des options « expertes » et parfois expérimentales qui permettent de jouer avec les détails de la théorie des types, que n'a pas Lean.

  • # Preuves de programme et preuves de théorèmes

    Posté par  . Évalué à 2 (+1/-0).

    Merci pour cette belle introduction à un sujet passionnément abstrait.

    Le titre parle d'assistant de preuve mais focalise surtout sur les preuves de programmes je comprends que c'est bien naturel sur ce site… Néanmoins avec Isabelle on glisse un peu vers la preuve purement 'mathématique' et le domaine inclut d'autres logiciels comme Mizar et Metamath qui me fascine depuis près de 30 ans de part sa simplicité théorique basée uniquement sur des substitutions.

    Metamath est la version informatique du livre illisible Principia Mathematica et permet d'admirer une preuve formelle de 2+2=4

    Les preuves de programmes ne sont pas toujours aussi fastidieuses mais le volume des démonstrations contribue dans les deux cas à dissuader leur usage. J'attends toujours l'automatisation qui rendra tous ces outils plus accessibles.

    • [^] # Re: Preuves de programme et preuves de théorèmes

      Posté par  (site web personnel, Mastodon) . Évalué à 2 (+0/-0). Dernière modification le 24 mars 2025 à 17:45.

      Notons tout de même que l'automatisation se développe énormément, d'abord la théorie des types en contient intrinsèquement une dose (l'égalité définitionnelle), ensuite Rocq comme Lean (et sûrement Agda, mais je connais moins bien) ont des tactiques qui font de la recherche automatique de preuve, et Lean a une tactique « simpl » très appréciée pour simplifier toutes sortes de buts. De manière plus générale, Rocq et Lean ont de grosses bibliothèques de tactiques (voir p.ex. https://rocq-prover.org/doc/V8.20.0/refman/coq-tacindex.html) pour faire plein d'étapes de preuve à la fois.

      Par exemple, la preuve de 2+2=4 en Lean est triviale (c'est un exemple d'égalité définitionnelle) :

      example : 2 + 2 = 4 := rfl
      
      • [^] # Re: Preuves de programme et preuves de théorèmes

        Posté par  . Évalué à 1 (+0/-0).

        Je ne prétends pas débattre avec le niveau requis, mais peut on encore parler de démonstration quand c'est "trivial" et que cela tient en une ligne ?

        De ce que je comprends il y a une sorte de consensus qui considère que les preuves formelles n'ont pas besoin d'aller au delà d'un certain niveau de détail. Les résultats "triviaux" n'ont pas à être démontrés et peuvent simplement être placés dans une bibliothèque. Intellectuellement ça me déçoit et en pratique cela introduit un risque de bug proportionnel à la taille de la "bibliothèque".

        • [^] # Re: Preuves de programme et preuves de théorèmes

          Posté par  (site web personnel, Mastodon) . Évalué à 3 (+1/-0).

          Je ne prétends pas débattre avec le niveau requis, mais peut on encore parler de démonstration quand c'est "trivial" et que cela tient en une ligne ?

          Oui, pourquoi pas ? De même que les maths ont fait un bond en avant quand zéro a été reconnu comme un vrai nombre, la logique marche mieux quand on reconnaît aussi les démonstrations triviales comme de vraies démonstrations :-)

          De ce que je comprends il y a une sorte de consensus qui considère que les preuves formelles n'ont pas besoin d'aller au delà d'un certain niveau de détail. Les résultats "triviaux" n'ont pas à être démontrés et peuvent simplement être placés dans une bibliothèque.

          Je ne sais pas d'où tu tires cette impression mais soit j'ai mal compris ce que tu veux dire, soit c'est faux.

          C'est quand même un peu le but de la preuve formelle que tout soit fait dans tous les détails y compris triviaux. Bien sûr, quand on est en plein développement, on peut laisser des lemmes triviaux comme admis pour les prouver plus tard, et il peut arriver qu'on les garde non prouvés dans le résultat fini, mais ce n'est pas commun (et quand c'est le cas, ça va normalement être mentionné explicitement).

          Les projets de formalisation réussis que j'ai mentionnés (retournement de la sphère, etc.) n'utilisent aucun lemme admis (seulement des axiomes « logiques » comme le tiers exclu).

          Et cette preuve « rfl » de 2+2=4 (plus généralement de l'égalité entre deux termes définitionnellement égaux) est bien une preuve, pas un appel à un lemme admis.

Envoyer un commentaire

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.