Sortie de Coq 8.5 bêta, un assistant de preuve formelle

L'assistant de preuve Coq, deux fois primé l'année dernière, vient de sortir en version 8.5 bêta. Attendue depuis plus d'un an déjà, on trouvera au menu de cette version un nombre certain de changements en profondeur.

Coq est un assistant de preuve sous licence LGPL 2.1, développé entre autres à l'INRIA. Issu des travaux sur la correspondance de Curry-Howard, Coq peut être vu aussi bien comme un langage de programmation que comme un système de preuves mathématiques. Il est, de fait, employé par les deux communautés. Parmi les développements en Coq, on peut citer par exemple le compilateur C certifié CompCert sur le versant informatique et la preuve du Théorème de Feit et Thompson sur le versant mathématique. Plus récemment, une des failles d'OpenSSL a été découverte grâce à Coq[^0] . Il est aussi de plus en plus utilisé comme système interactif pour l'apprentissage de la logique dans l'enseignement supérieur.

On rappellera dans le reste de la dépêche les grands principes qui sous-tendent Coq, ce qu'il est, ce qu'il n'est pas, puis on détaillera les changements introduits dans cette version.

Sommaire

• Coq, en résumé
  • Les logiciels de méthodes formelles
  • Un assistant de preuve
  • Écosystème
  • Usage industriel
• Quelques nouveautés de Coq 8.5
• Preuves et programmes : deux faces de la même pièce
  • Un peu d'histoire
  • Les grands ancêtres
  • Des systèmes de types aux systèmes de preuves
  • De nouvelles fondations
  • Méli-mélo de Coq au Curry-Howard
  • Un langage exotique
• Le futur ?
  • Notes

Coq, en résumé

Développé depuis trois décennies, la version 1 datant de 1984, Coq vient d'être consacré dans la cour des grands l'année dernière, en recevant le très prestigieux prix ACM Software System Award de l'ACM, côtoyant ainsi Unix, TCP/IP, TeX, Java, Make et d'autres grands noms faisant partie de notre quotidien  —  LLVM avait ainsi été récompensé l'année précédente.

Les logiciels de méthodes formelles

Un « assistant de preuve » fait partie d'une famille plus large de logiciels visant à établir la vérité (ou la fausseté) d'un énoncé mathématique donné. Par exemple, une égalité entre deux expressions mathématiques, ou un énoncé décrivant le fait qu'un certain système formalisé ne tombe jamais dans un état de panne, ou encore le fait qu'il existe une infinité de nombres premiers. Il existe une grande diversité d'approches selon la nature des énoncés concernés et la nature plus ou moins automatique de l'obtention du résultat :

• On parle de « prouveurs automatiques de théorèmes » pour les logiciels très automatisés qui prennent l'énoncé en entrée et répondent soit « vrai », soit « faux », soit parfois « je ne sais pas » sans aucune information supplémentaire. Par exemple, les solveurs SAT ou SMT essaient de prouver des énoncés logiques utilisant un langage restreint (logique pure, arithmétique, tableaux, un peu de quantificateur, …). Ils ne savent répondre automatiquement que si la réponse peut être trouvée de façon assez « bête », mais peuvent traiter des formules énormes qu'un humain ne saurait pas manipuler ; ils sont donc de plus en plus utilisés dans l'industrie. Le model checking utilise ces outils pour vérifier automatiquement des propriétés de systèmes physiques ou virtuels ayant un nombre d'états possibles fini.

• Les « analyseurs de programmes » sont une classe d'outils spécialisés pour l'étude des programmes informatiques. Les systèmes de typage statiques en font partie, mais aussi par exemple les outils utilisant l'interprétation abstraite. Ils peuvent garantir l'absence d'une classe d'erreurs variées, allant de l'absence de confusion pointeurs/entiers à l'absence de division par zéro, par exemple. Certains outils permettent d'annoter les programmes avec des invariants et contrats supplémentaires pour prouver des propriétés plus proches encore de la spécification formelle du programme.

• Les « assistants de preuves » sont des logiciels qui permettent de manipuler des énoncés trop compliqués pour que l'ordinateur les vérifie seul. Ils se présentent comme un langage qui permet de décrire à l'ordinateur non pas un programme informatique, mais les étapes de raisonnement pour justifier un énoncé mathématique. Si le code fourni est accepté par l'assistant, la preuve est correcte et l'énoncé est vrai.

La plupart des théories mathématiques et des énoncés concernant des langages de programmation Turing-complets, ne sont pas décidables automatiquement (il n'existe pas d'algorithme qui peut toujours répondre « oui » ou « non » sans se tromper). Les outils de preuve automatique ont donc toujours un risque de répondre « je ne sais pas ». De même, quand on conçoit un outil d'analyse de programme, il faut accepter qu'il « ne sache pas » dans certains cas ; selon ses priorités, on décidera alors de rejeter des programmes valides (si on veut garantir l'absence d'erreur) ou d'accepter des programmes incorrects (si on veut prévenir l'utilisateur seulement quand il y a vraiment une erreur).

Si on veut pouvoir travailler sur des énoncés mathématiques ou programmes quelconques, une idée de plus en plus réaliste est d'utiliser les assistants de preuve pour décrire les parties difficiles d'une preuve, et laisser des prouveurs plus automatiques décider les sous-parties les plus évidentes. Ou bien utiliser un outil d'analyse de programme, mais faire parfois appel à un assistant de preuve sur les quelques cas trop difficiles à gérer entièrement automatiquement.

Un assistant de preuve

Coq est un assistant de preuve. Il manipule des preuves, dans un sens mathématique. L'utilisateur énonce des théorèmes et il doit ensuite fournir une preuve formelle de ceux-ci, sous forme d'étapes de raisonnement élémentaires dans la plupart des cas. Une fois la preuve donnée, le logiciel vérifie qu'il s'agit bien d'une preuve correcte, sans erreur de raisonnement, puis la marque comme validée. On peut ainsi construire de manière incrémentale une bibliothèque de preuves vérifiées mécaniquement par ordinateur.

Le choix de la dénomination « bibliothèque » dans la phrase précédente n'est pas due au hasard. Pour une raison fondamentale, dont on discutera par la suite, l'ingénierie de la preuve est très similaire à l'ingénierie logicielle. Pour l'instant, il est raisonnable de se figurer que des preuves dépendent d'autres preuves de la même manière que les fonctions d'un programme dépendent de fonctions définies auparavant.

Coq est un assistant de preuve, mais c'est aussi un langage de programmation. En particulier, il fournit un système de modules qui ressemble à celui d'OCaml. L'exemple qui suit définit une fonction multiplicity récursive (mot-clé Fixpoint) qui renvoie le nombre de fois qu'apparaît l'entier n dans une liste l. Ensuite il prouve une propriété simple sur la fonction : la multiplicité de n dans la concaténation de deux listes est la somme des multiplicités de n dans chaque liste.

(* import de modules pour les listes et l'arithmétique *)
Require Import List Arith.
Fixpoint multiplicity (n : nat) (l : list nat) : nat  :=
    (* filtrage par motifs sur la liste "l" *)
    match l with       
    (* cas où la liste est vide *)
    | nil     => 0  
    (* cas où on a un élément "a" en tête de liste, "l'" le reste *)  
    | a :: l' => 
        (* test d'égalité de "n" avec l'élément "a" *)       
        if eq_nat_dec n a             
        (* appel récursif suivi de la fonction successeur d'un entier *)
        then S (multiplicity n l')  
        else multiplicity n l'         
    end.

Lemma multiplicity_app (n : nat) (l1 l2 : list nat) : 
  multiplicity n (l1 ++ l2) = multiplicity n l1 + multiplicity n l2.
Proof.
  induction l1. reflexivity.
  simpl. destruct eq_nat_dec; auto.
  rewrite IHl1. auto.
Qed.

Une des caractéristiques des fonctions récursives en Coq, liée au fait que Coq n'est pas Turing-Complet, est qu'elles terminent — ou autrement dit, s'arrêtent forcément à un moment donné. En effet, Coq vérifie que les arguments de l'appel récursif sont plus petits : il accepte l'exemple, car la liste l' est obtenue à partir de la liste l en lui enlevant son premier élément. Il arrive que certaines fonctions récursives terminent, mais que Coq ne soit pas capable de le deviner : savoir si un objet est plus petit qu'un autre n'est pas toujours évident. Dans ces cas, il faut l'aider un peu pour qu'il accepte la fonction.

Voici deux preuves plus compliquées, reposant sur des définitions précédentes et bibliothèques de théorèmes. La première énonce qu'un petit langage de programmation est déterministe : si le programme c, partant de l'état mémoire st, peut arriver soit dans l'état st1 soit dans l'état st2, alors ces deux états sont égaux.

Theorem ceval_deterministic: ∀c st st1 st2,
  c / st ⇓ st1 →
  c / st ⇓ st2 →
  st1 = st2.
Proof.
  introv E1 E2. gen st2.
  induction E1; intros; inverts× E2; tryfalse.
  forwards*: IHE1_1. subst×.
  forwards*: IHE1_1. subst×.
Qed.

La seconde fait partie d'une preuve qu'il y a une infinité de nombres premiers : pour tout nombre entier m, on peut trouver un nombre entier premier p strictement supérieur à m.

Lemma prime_inf m : {p | m < p & prime p}.
Proof.
  pose c := pdiv m`!.+1.
  have Pc : prime c by apply/pdiv_prime/fact_gt0.
  exists c => //.
  have [cLm|//] := leqP.
  have /Euclid_dvd1 := Pc.
  have /eqP<- := coprimenS (m`!).
  rewrite dvdn_gcd pdiv_dvd.
  by have /fact_div-> : 0 < pdiv m`!.+1 <= m by rewrite prime_gt0.
Qed.

Écosystème

À l'instar des langages de programmation, il existe différents assistants de preuves, qui ne reposent pas tous sur la même base théorique, diffèrent au niveau de la syntaxe ou de l'expressivité. Citons quelques noms à la louche :

• ACL2 ;
• PVS ;
• La famille HOL (HOL4, HOL Light…) ;
• Isabelle, successeur de HOL ;
• Agda, qui est probablement l'un des plus proches cousins de Coq à l'état naturel.

La preuve assistée par ordinateur est une pratique qui se répand de plus en plus, avec aussi bien des théorèmes légendaires formalisés que des systèmes informatiques complexes certifiés sans bugs. Citons deux projets époustouflants et révélateurs de ce qui se fait déjà à l'heure actuelle :

• Le projet Flyspeck, en HOL Light sous licence BSD, qui visait à prouver la conjecture de Kepler, vient d'arriver à son terme l'été dernier. Cette conjecture, évidente pour n'importe quel vendeur d'oranges, avait tout de même été énoncée en 1611 !
• Le système d'exploitation seL4 prouvé de bout en bout en Isabelle (et open sourcé GPL / BSD, de surcroît).

Parmi les gros développements en Coq, on peut citer :

• Le théorème des quatre couleurs, prouvé en 2008 (45 kloc, licence non-spécifiée, code source) ;
• Le théorème de Feit et Thompson, prouvé en 2012 (170 kloc, CECILL-B, code source) ;
• CompCert, un compilateur C certifié (110 kloc, hélas, une partie du code source est réservé aux utilisations non-commerciales uniquement) ;
• Bedrock, un cadriciel de preuve de programmes (BSD, code source).

Il faut savoir que les deux premiers théorèmes ont été prouvés par Georges Gonthier et son équipe, après une quantité impressionnante de travail acharné (6 ans pour Feit-Thompson).

Usage industriel

Les débouchés industriels des outils de preuve formelle sont nombreux. L'industrie a adopté en premier les outils de démonstration automatique et de model checking qui sont les plus automatisés et donc les plus faciles à utiliser (voir par exemple l'article A short survey of automated reasoning de John Harrison, 2007). Par exemple, les concepteurs de micro-processeurs utilisent très lourdement des outils de vérification formelle pour garantir la correction des futurs modèles à différents moments de leur conception.

Les assistants de preuves ont longtemps été réservés à un usage par une petite poignée d'experts (utilisation de la méthode B sur le logiciel critique embarqué de la ligne 14 de métro automatique), mais commencent à se diffuser. En particulier, les industries manipulant des logiciels critiques s'intéressent aux logiciels prouvés corrects utilisant ces méthodes. Par exemple, Airbus s'intéresse à l'usage du compilateur prouvé correct Compcert. Le micro-noyau Sel4 (prouvé correct avec l'assistant Isabelle) a lui été utilisé par un groupe de chercheurs et d'industriels pour construire l'hélicoptère télécommandé « le plus sécurisé au monde » (un projet qui intéresse beaucoup les militaires…).

Quelques nouveautés de Coq 8.5

Plus de deux ans et demi après la version 8.4, sortie en août 2012, la version 8.5 de Coq marque de grands changements. Elle intègre en effet quatre branches apportant des fonctionnalités remarquables.

• Sous le capot, le moteur de tactiques (recherche de preuve) a été refait de fond en comble. Le langage de surface a été changé le moins possible, mais cela constitue une nouvelle base qui ouvre la voie à des changements / structurations / simplifications importantes dans le futur. (Arnaud Spiwack)
• Le modèle de compilation / vérification des preuves est maintenant asynchrone ; au lieu de vérifier un fichier de preuves ligne par ligne, Coq trace maintenant les dépendances pour calculer en parallèle les résultats indépendants, et recalculer incrémentalement ce qui est nécessaire après un changement. (Enrico Tassi)
• un nouveau mécanisme d'évaluation des termes, native_compute est disponible : au lieu d'interpréter le calcul ou de le compiler vers un bytecode, il produit des programmes OCaml qui sont compilés à la volée en code natif. Ce mécanisme accélère beaucoup les très gros calculs, mais n'est pas rentable pour les opérations simples où le coût de compilation dominerait. (Maxime Dénès)
• La logique sous-jacente a été étendue avec de nouvelles notions avancées : polymorphisme d'univers (plus modulaire) et projections natives (plus efficace). (Matthieu Sozeau)

Quelques autres changements importants sont:

• Une construction $(...)$ qui permet d'intégrer des bouts de tactique directement dans des programmes  —  on ne pouvait auparavant faire que l'inverse avec la tactice refine. C'est très très pratique.
• Une restriction de la condition de garde (qui vérifie que les programmes terminent) pour corriger une incompatibilité de la logique avec des axiomes désirables (l'extensionnalité des propositions, et des conséquences de l'univalence).
• Une nouvelle option -type-in-type qui rend la logique incohérente (on peut prouver False) mais est pratique pour prototyper des idées sans avoir à gérer les niveau d'univers dans un premier temps.
• Une tactique cbn qui remplace avantagement simpl.
• Un nouveau motif introductif = x1 .. xn qui applique injection au vol (inspiré de SSReflect, un jeu alternatif de tactiques de base pour Coq)
• De nouvelles constructions uconstr:c et type_term c pour programmer des tactiques manipulant des termes pas encore typés.

Le Changelog complet est disponible. La partie cachée de l'iceberg contient de nombreuses modifications et bugfixes (avec en particulier Pierre Boutillier, Hugo Herbelin, Pierre Letouzey et Pierre-Marie Pédrot).

Preuves et programmes : deux faces de la même pièce

Cette partie plus historique détaille un aspect important et intéressant de la conception de l'assistant de preuve Coq, qui repose sur une correspondance entre preuves et programmes. Attention à ne pas en faire une idéologie : tous les assistants de preuve ne reposent pas sur ces mêmes bases, et les bons outils obtenus aujourd'hui sont au final assez proches à l'usage, quelle que soit leur tradition scientifique.

Coq possède une particularité que ne présentent pas la majorité des autres assistants de preuve : il est basé sur la fameuse correspondance de Curry-Howard. Sous ce nom à priori barbare se cache une révolution paradigmatique de la logique, d'importance probablement comparable à l'introduction de la relativité générale en physique. Par un remarquable double effet Kiss-Cool, cette révolution est aussi d'une importance capitale pour l'informatique[^1] !

Un peu d'histoire

Pour avoir une idée de l'importance de cette révolution, je me permets de faire un détour par la logique, en espérant ne pas perdre le valeureux lecteur en route. Revenons pour cela quelques malheureux 2500 ans en arrière.

À cette époque, un type nommé Aristote cherche à justifier le raisonnement logique conduisant à produire des énoncés vrais. La logique de cette époque est en effet essentiellement perçue à travers le prisme du langage et de la rhétorique, d'où le nom même de « logique », qui vient en fait du mot λόγος (logos) signifiant « parole ».

Ce nommé Aristote écrit l'Organon, qui deviendra jusqu'au XIXe siècle à la logique ce que The C Programming Language est au langage C. On y apprend des choses fort intéressantes, dont voici un exemple afin d'en jauger la teneur :

• Socrate est un homme.
• Tous les hommes sont mortels.
• Donc Socrate est mortel.

Si l'Organon a fait le délice des étudiants en scolastique médiévaux, il faut attendre la fin du XIX^è siècle pour que les mathématiques s'emparent vraiment de la logique comme un objet à étudier formellement. Commence alors le règne encore inachevé de la théorie des ensembles.

Les grands ancêtres

Le début du XXe siècle est une période fertile pour les progrès de la logique formelle[^2]. Le développement du logicisme permet l'élaboration incrémentale d'une théorie permettant de décrire les théories mathématiques sans ambiguïté ni possibilité d'erreurs : la théorie des ensembles. L'histoire n'étant pas un long fleuve tranquille, la formulation de cette théorie fut plusieurs fois mise en défaut. Un des paradoxes les plus connus et les plus simples à expliquer est sans aucun doute le paradoxe de Russell, publié en 1903. Malgré sa mise en équations, la logique conserve alors encore sa nature aristotélicienne, c'est-à-dire qu'on pouvait la résumer à un ensemble de règles à appliquer qui garantissent la correction du raisonnement.

À peu près à la même époque et pour des raisons liées, se posent les premières questions de la définition de ce qu'on appellait alors « méthodes effectives », mais que l'on appellerait plus volontiers aujourd'hui « algorithmes ». Plusieurs tentatives de création de systèmes capturant physiquement la notion abstraite de calcul mènent à l'élaboration de deux célèbres modèles de calcul encore utilisés de nos jours.

• Les machines de Turing, inventées par Alan Turing en 1936.
• Le λ-calcul, dû à Alonzo Church, daté des années 30.

Si les machines de Turing peuvent être vaguement considérées comme la source d'inspiration des langages de programmation impératifs, le λ-calcul est quant à lui l'ancêtre direct des langages de programmation fonctionnels. Les deux paradigmes ont rapidement été démontrés équivalents, menant à la notion de Turing-complétude. Un langage est dit Turing-complet s'il est aussi expressif qu'une machine de Turing  —  ou que le lambda-calcul. Cela signifie qu'on peut y écrire tous les algorithmes raisonnables.

Des systèmes de types aux systèmes de preuves

Les premiers langages fonctionnels comme LISP ne présentaient pas de systèmes de types statiques, conduisant à une sémantique similaires aux langages dynamiques comme Python. Étonnamment, s'il faut attendre 1972 et la publication du langage ML pour obtenir un système de types satisfaisant pour l'usage quotidien, le λ-calcul avait été doté quasiment dès ses origines d'un système de types simple. ML a justement été conçu comme langage pour programmer l'un des premiers assistants de preuves, LCF, et son typage servait à garantir que les utilisateurs ne pouvaient pas manipuler le langage pour fabriquer de « fausses preuves » d'un énoncé. Coq poursuit cette tradition : c'est un descendant de LCF implémenté dans un descendant de ce ML des origines.

La correspondance de Curry-Howard est la découverte fortuite par Haskell Curry en 1958 puis William Alvin Howard en 1969 que le système de types primitif du λ-calcul correspondait en fait exactement à un système logique minimaliste, la bien nommée logique propositionnelle minimale. C'était là la découverte d'une véritable pierre de Rosette des fondements de l'informatique, comblant le fossé qui séparait la théorie de la calculabilité (et de là l'informatique) avec la logique mathématique (et avec elle les mathématiques).

La correspondance de Curry-Howard énonce ainsi que :

• Les preuves mathématiques sont les programmes des langages fonctionnels ;
• Les formules logiques que démontrent ces preuves sont les types de ces programmes.

Il ne s'agit pas d'une vague ressemblance : dès lors qu'on a trouvé le bon angle sous lesquels les regarder, ces objets sont exactement les mêmes. Ainsi, on peut donner quelques traductions à travers cette pierre de Rosette pour éclairer le lecteur perdu.

Informatique	Mathématiques
Type	Formule
Programme	Preuve
Primitive système	Axiome
Fonction de A vers B	Preuve de « A implique B »
Paire de A et B	Preuve de « A et B »
Type somme sur A et B	Preuve de « A ou B »
Interpréteur	Théorème de correction
Décompilateur	Théorème de complétude

Un des intérêts de cette équivalence est que l'on peut faire des va-et-vient d'un monde à l'autre. Ainsi, certaines primitives venant de la programmation sont traduites comme des lois logiques nouvelles et inversement. Ce changement paradigmatique marque aussi la naissance de la théorie de la démonstration moderne. Puisque les preuves sont des programmes, elles calculent et, donc, deviennent intéressantes en soi.

De nouvelles fondations

Peu à peu, des systèmes logiques de plus en plus riches se sont développés sur ce terreau fertile. Coq est ainsi une extension du calcul des constructions (de son petit nom CoC) développé par Thierry Coquand à la fin des années 1980. Il convient de citer aussi la théorie des types de Martin-Löf (MLTT), qui lui est similaire, sur laquelle se base Agda.

Ce courant de recherche se veut une alternative à la théorie des ensembles du siècle passé, permettant d'unifier logique et calcul en un seul et même formalisme. Le recours à l'ordinateur laisse aussi espérer l'adaptation des techniques du génie logiciel au génie de la preuve, et le passage à l'échelle des mathématiques.

Tout récemment, le petit monde de la théorie de la démonstration a été secoué par les idées de Vladimir Voïevodski, médaille Fields 2002, qui s'est rendu compte que la théorie des types était un excellent langage pour écrire les preuves d'homotopie. La théorie homotopique des types (HoTT) était née. Coq est un des langages dans laquelle cette théorie est implémentée. On pourra se réferer au pavé collaboratif de quelques 600 pages, le HoTT Book[^4].

Méli-mélo de Coq au Curry-Howard

Coq est le résultat de ce courant de recherche fondamentale. En effet, il n'y a pas de différence formelle en Coq entre une preuve et un programme. Les deux objets vivent dans le même langage, à tel point qu'on peut calculer avec une preuve et, inversement, enrichir un programme avec des morceaux de preuves. Voici un exemple très simple de la fonction prédécesseur :

Definition pred : forall n : nat, {m : nat | n = 0 \/ n = S m} :=
fun (n : nat) =>
(** analyse de cas sur n *)
match n return {m : nat | n = 0 \/ n = S m} with
(** n vaut zéro *)
| 0 => exist _ 0 (or_introl eq_refl)
(** n est de la forme n' + 1 *)
| S n' => exist _ n' (or_intror eq_refl)
end.

Ce fragment se lit ainsi :

• Version informatique : on définit la fonction pred qui prend en argument un entier naturel n et qui renvoie un entier naturel m tel que soit n vaut zéro, soit n = m + 1.
• Version mathématique : le théorème pred affirme que pour tout entier naturel n, il existe un entier naturel m tel que n vaut zéro ou n = m + 1.

Et effectivement, on peut calculer le résultat de l'application de cette fonction-théorème (proj1_sig est la fonction qui extrait le témoin de l'existentielle).

Eval compute in proj1_sig (pred 42).
     = 41
     : nat

Coq propose aussi un langage externe dit « de tactiques » qui permet d'écrire des preuves par méta-programmation, appelé Ltac. Un script de preuve n'est pas une preuve, c'est un programme qui manipule des morceaux de preuves pour construire un terme de preuve. Malheureusement, on ne sait pas encore concevoir des langages propres pour faire cela, et le langage actuel est impératif, non-typé et mal compris. Le résultat est aussi sordide que le langage interne de Coq est élégant. On pourra se le figurer comme l'hybride démoniaque entre TeX et PHP, pour les connaisseurs. Le programme précédent peut s'écrire à l'aide de Ltac comme suit.

Definition pred : forall n : nat, {m : nat | n = 0 \/ n = S m}.
Proof.
intros n; destruct n.
+ exists 0; left; reflexivity.
+ exists n; right; reflexivity.
Defined.

Le terme produit par cette séquence de commandes est le même que celui qu'on a écrit à la main auparavant. L'avantage de Ltac est qu'il permet d'écrire des morceaux de preuves aisément, au prix d'un moins grand contrôle sur le terme produit.

Agda, le seul autre assistant de preuve mainstream aussi proche de l'idée de correspondance preuve-programme, a fait un choix différent, qui est de n'avoir qu'un langage de termes (et pas de méta-programmes), et d'essayer de le rendre le plus propre possible pour permettre de l'utiliser directement. Cela a conduit à des idées intéressantes, mais pour l'instant le résultat est moins adapté à l'automatisation des preuves et donc aux formalisations de grande ampleur. (Les utilisateurs Agda essaient de compenser par un mode Emacs de folie qui ré-écrit les termes de preuve pour eux; il y a du bon et du moins bon dans cette approche.)

Un langage exotique

En tant que langage de programmation, Coq fait malgré tout figure d'alien aux yeux des programmeurs lambda.

En premier lieu, Coq est un langage de programmation purement fonctionnel, et ce, encore plus que Haskell. Il n'y a en effet aucun effet de bord possible et cela inclut aussi bien la mémoire mutable que l'affichage sur la ligne de commande. Eh oui, on ne peut même pas écrire le Hello World des familles en Coq ! Imaginez le désarroi de ses promoteurs quand on le leur demande… Pas non plus d'exceptions, de primitives systèmes, etc. On peut cependant toujours se débrouiller en encodant ces effets dans une monade, comme en Haskell.

Pire encore, quand nous disons que Coq est plus pur que Haskell, cela n'est pas pour rien. Il est en effet impossible en Coq d'écrire un programme qui ne termine pas. Coq est très strict sur les fonctions qu'il accepte et demande souvent un peu de gymnastique au programmeur. Le point positif de cette rigidité est que les programmes sont garantis de respecter leur spécification. En un sens, Coq rend vrai l'adage souvent appliqué à OCaml et à Haskell : « quand ça compile, c'est que ça marche ».

Une conséquence inattendue de ce fait : Coq n'est pas Turing-complet. Il existe donc des programmes qu'on ne peut pas écrire en Coq. Ce n'est pas un bug, c'est une feature ! Cette restriction permet de passer outre les limitations dues au théorème d'incomplétude de Gödel  —  mais complique l'écriture de programme dont on ne sait pas prouver la terminaison ou la productivité^[3].

Le futur ?

Les gens qui travaillent sur les assistants de preuves imaginent un monde où les mathématiciens et mathématiciennes travaillent directement avec des assistants de preuve et où l'on n'a plus jamais besoin de corriger un résultat qui s'avère faux après sa publication. C'est encore une utopie, même si les mathématiciens sont de plus en plus nombreux à prendre ces outils au sérieux. Aujourd'hui, les assistants de preuves restent trop difficiles à utiliser pour des « mathématiques de tous les jours » et il faudra encore des efforts de simplification et d'ergonomie pour rendre cette idée réaliste.

Des bibliothèques importantes de mathématiques formalisées existent déjà (par exemple le journal Formalized Mathematics présente les nombreux résultats formalisés dans la Mizar Mathematical Library), mais elles soulèvent de nombreuses questions d'ingénérie des preuves et d'inter-opérabilité entre les différents langages de description de preuves.

La formalisation assistée par ordinateur laisse malgré tout entrevoir la possibilité de faire des mathématiques que l'esprit humain ne saurait appréhender aisément aujourd'hui. Ainsi, une des barrières à la preuve, aussi bien du théorème des quatre couleurs que de la conjecture de Kepler, était la quantité dantesque de cas particuliers à vérifier à la main, que l'ordinateur a pu traiter rapidement. Une nouvelle ère des mathématiques est probablement en train de s'ouvrir sous nos yeux.

Par ailleurs, on voit fleurir des outils permettant de vérifier formellement que les programmes informatiques respectent une spécification. Alors qu'on peut imaginer que les preuves mathématiques aient toute vocation à être vérifiées, personne ou presque n'espère réellement que tous les logiciels écrits soient un jour prouvés corrects. D'une part, certains logiciels n'ont pas de spécification claire, stable ou que l'on sait exprimer (comment spécifier un économiseur d'écran ?) ; d'autre part, les facteurs économiques jouent contre les preuves formelles. En effet, même si la preuve formelle devenait un jour la façon la plus économique d'éviter les bugs dans les logiciels, cela restera toujours plus difficile et donc plus coûteux que d'écrire du logiciel buggué. On peut cependant rêver au fait que, d'ici quelques dizaines d'années, le dessous de l'iceberg (les bibliothèques standards, compilateurs, runtime, noyaux de système d'exploitation ou navigateurs web) sur lequel reposent les programmes grand-publics soient spécifiés le plus précisément possible et prouvés corrects par rapport à cette spécification.

L'assistant de preuve Coq, en permettant à chacun de se former à la preuve formelle (ou à la preuve tout court) et de se lancer dans des formalisations qui commencent à être de grande ampleur, est un des outils phare de cette (r)évolution.

Notes

^[0] Plus précisément, c'est en cherchant à modéliser ce sous-système dans Coq que Masashi Kikuchi a découvert ce défaut de conception. La démarche de la preuve formelle revient à soumettre tout un système à un tyran de rigueur insatiable. Il révèle ses erreurs, ses points faibles et force l'utilisateur à une compréhension au centimètre près. Si la présentation n'est pas structurée et élégante, la preuve en est d'autant plus difficile. Les assistants de preuves poussent à la simplicité et permettent souvent la production de documents pédagogiques remarquables, car leur clarté vient non des détails qu'ils passent sous le tapis, mais de la rigueur qui leur a été imposée. C'est souvent dans un article de la forme Comment prouver formellement X que vous trouverez l'exposition la plus claire du sujet X.

^[1] Peut-être presque autant que la sortie de l'iPhone n + 1, pour un n bien choisi.

^[2] Je recommande la lecture de la captivante BD Logicomix à ceux qui sont intéressés.

^[3] Dans les faits, 99,99% des programmes imaginables peuvent s'écrire en Coq. On dit aussi souvent que cela empêche aussi d'écrire un interpréteur de Coq en Coq, mais cela est plus compliqué en pratique. On pourrait écrire une fonction qui effectue une étape de réduction (et laisser l'utilisateur pédaler), ou imaginer bootstrapper à l'aide d'un axiome bien choisi.

^[4]Quand un mathématicien déclare son amour à git et à l'esprit du libre.

Aller plus loin

• Page officielle (470 clics)
• ACM Software System Award (44 clics)
• ACM Programming Languages Software Award (38 clics)
• Le compilateur C certifié CompCert (105 clics)
• Annonce de la preuve du théorème de Feit-Thompson en Coq (77 clics)
• Historique du développement de Coq (162 clics)
• Annonce officielle de la bêta (49 clics)