tag:linuxfr.org,2005:/users/perthmad/newsLinuxFr.org : les dépêches de Perthmâd2015-02-26T21:41:03+01:00/favicon.pngtag:linuxfr.org,2005:News/360402015-01-28T09:44:35+01:002015-01-29T08:45:56+01:00Sortie de Coq 8.5 bêta, un assistant de preuve formelleLicence CC By‑SA http://creativecommons.org/licenses/by-sa/4.0/deed.fr<div><p>L'assistant de preuve <a href="https://coq.inria.fr/">Coq</a>, 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.</p>
<p>Coq est un assistant de preuve sous licence LGPL 2.1, développé entre autres à l'INRIA. Issu des travaux sur la <a href="https://fr.wikipedia.org/wiki/correspondance%20de%20Curry-Howard" title="Définition Wikipédia">correspondance de Curry-Howard</a>, 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é <a href="https://fr.wikipedia.org/wiki/CompCert" title="Définition Wikipédia">CompCert</a> sur le versant informatique et la preuve du <a href="https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me%20de%20Feit%20et%20Thompson" title="Définition Wikipédia">Théorème de Feit et Thompson</a> sur le versant mathématique. Plus récemment, <a href="http://ccsinjection.lepidum.co.jp/blog/2014-06-05/CCS-Injection-en/index.html">une des failles d'OpenSSL a été découverte grâce à Coq</a>[<sup>0]</sup> . Il est aussi de plus en plus utilisé comme système interactif pour l'apprentissage de la logique dans l'enseignement supérieur.</p>
<p>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.</p></div><ul><li>lien nᵒ 1 : <a title="https://coq.inria.fr/" hreflang="en" href="https://linuxfr.org/redirect/92800">Page officielle</a></li><li>lien nᵒ 2 : <a title="http://awards.acm.org/software_system/" hreflang="en" href="https://linuxfr.org/redirect/92801">ACM Software System Award</a></li><li>lien nᵒ 3 : <a title="http://www.sigplan.org/Awards/Software/" hreflang="en" href="https://linuxfr.org/redirect/92802">ACM Programming Languages Software Award</a></li><li>lien nᵒ 4 : <a title="http://compcert.inria.fr/" hreflang="en" href="https://linuxfr.org/redirect/92803">Le compilateur C certifié CompCert</a></li><li>lien nᵒ 5 : <a title="http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/" hreflang="en" href="https://linuxfr.org/redirect/92804">Annonce de la preuve du théorème de Feit-Thompson en Coq</a></li><li>lien nᵒ 6 : <a title="https://www.inria.fr/innovation/secteurs-industriels/edition-de-logiciels-systemes-embarques/demos/coq/chronologie" hreflang="fr" href="https://linuxfr.org/redirect/92805">Historique du développement de Coq</a></li><li>lien nᵒ 7 : <a title="https://coq.inria.fr/news/123.html" hreflang="en" href="https://linuxfr.org/redirect/92931">Annonce officielle de la bêta</a></li></ul><div><h2 class="sommaire">Sommaire</h2>
<ul class="toc">
<li>
<a href="#coq-en-r%C3%A9sum%C3%A9">Coq, en résumé</a><ul>
<li><a href="#les-logiciels-de-m%C3%A9thodes-formelles">Les logiciels de méthodes formelles</a></li>
<li><a href="#un-assistant-de-preuve">Un assistant de preuve</a></li>
<li><a href="#%C3%89cosyst%C3%A8me">Écosystème</a></li>
<li><a href="#usage-industriel">Usage industriel</a></li>
</ul>
</li>
<li><a href="#quelques-nouveaut%C3%A9s-de-coq-85">Quelques nouveautés de Coq 8.5</a></li>
<li>
<a href="#preuves-et-programmes--deux-faces-de-la-m%C3%AAme-pi%C3%A8ce">Preuves et programmes : deux faces de la même pièce</a><ul>
<li><a href="#un-peu-dhistoire">Un peu d'histoire</a></li>
<li><a href="#les-grands-anc%C3%AAtres">Les grands ancêtres</a></li>
<li><a href="#des-syst%C3%A8mes-de-types-aux-syst%C3%A8mes-de-preuves">Des systèmes de types aux systèmes de preuves</a></li>
<li><a href="#de-nouvelles-fondations">De nouvelles fondations</a></li>
<li><a href="#m%C3%A9li-m%C3%A9lo-de-coq-au-curry-howard">Méli-mélo de Coq au Curry-Howard</a></li>
<li><a href="#un-langage-exotique">Un langage exotique</a></li>
</ul>
</li>
<li>
<a href="#le-futur">Le futur ?</a><ul>
<li><a href="#notes">Notes</a></li>
</ul>
</li>
</ul><h2 id="coq-en-résumé">Coq, en résumé</h2>
<p>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 <a href="http://en.wikipedia.org/wiki/ACM_Software_System_Award" title="Définition Wikipédia">ACM Software System Award</a> de l'<a href="http://fr.wikipedia.org/wiki/Association_for_Computing_Machinery" title="Définition Wikipédia">ACM</a>, 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.</p>
<h3 id="les-logiciels-de-méthodes-formelles">Les logiciels de méthodes formelles</h3>
<p>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 :</p>
<ul>
<li><p>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 <a href="http://fr.wikipedia.org/wiki/Probl%C3%A8me_SAT">SAT</a> ou <a href="http://fr.wikipedia.org/wiki/Satisfiability_Modulo_Theories_%28SMT%29">SMT</a> 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 <a href="https://fr.wikipedia.org/wiki/model%20checking" title="Définition Wikipédia">model checking</a> utilise ces outils pour vérifier automatiquement des propriétés de systèmes physiques ou virtuels ayant un nombre d'états possibles fini.</p></li>
<li><p>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'<a href="http://fr.wikipedia.org/wiki/Interpr%C3%A9tation_abstraite">interprétation abstraite</a>. 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.</p></li>
<li><p>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.</p></li>
</ul><p>La plupart des théories mathématiques et des énoncés concernant des langages de programmation <a href="http://fr.wikipedia.org/wiki/Turing-complet">Turing-complets</a>, 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).</p>
<p>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.</p>
<h3 id="un-assistant-de-preuve">Un assistant de preuve</h3>
<p>Coq est un <strong>assistant de preuve</strong>. 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.</p>
<p>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.</p>
<p>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'<a href="http://fr.wikipedia.org/wiki/OCaml">OCaml</a>. L'exemple qui suit définit une fonction <code>multiplicity</code> récursive (mot-clé <code>Fixpoint</code>) qui renvoie le nombre de fois qu'apparaît l'entier <code>n</code> dans une liste <code>l</code>. Ensuite il prouve une propriété simple sur la fonction : la multiplicité de <code>n</code> dans la concaténation de deux listes est la somme des multiplicités de <code>n</code> dans chaque liste.</p>
<pre><code class="coq"><span class="c">(* import de modules pour les listes et l'arithmétique *)</span>
<span class="kn">Require</span> <span class="kn">Import</span> <span class="nc">List</span> <span class="nn">Arith</span><span class="p">.</span>
<span class="nc">Fixpoint</span> <span class="n">multiplicity</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">nat</span><span class="o">)</span> <span class="o">(</span><span class="n">l</span> <span class="o">:</span> <span class="kt">list</span> <span class="n">nat</span><span class="o">)</span> <span class="o">:</span> <span class="n">nat</span> <span class="o">:=</span>
<span class="c">(* filtrage par motifs sur la liste "l" *)</span>
<span class="k">match</span> <span class="n">l</span> <span class="k">with</span>
<span class="c">(* cas où la liste est vide *)</span>
<span class="o">|</span> <span class="n">nil</span> <span class="o">=></span> <span class="mi">0</span>
<span class="c">(* cas où on a un élément "a" en tête de liste, "l'" le reste *)</span>
<span class="o">|</span> <span class="n">a</span> <span class="o">::</span> <span class="n">l'</span> <span class="o">=></span>
<span class="c">(* test d'égalité de "n" avec l'élément "a" *)</span>
<span class="k">if</span> <span class="n">eq_nat_dec</span> <span class="n">n</span> <span class="n">a</span>
<span class="c">(* appel récursif suivi de la fonction successeur d'un entier *)</span>
<span class="k">then</span> <span class="nc">S</span> <span class="o">(</span><span class="n">multiplicity</span> <span class="n">n</span> <span class="n">l'</span><span class="o">)</span>
<span class="k">else</span> <span class="n">multiplicity</span> <span class="n">n</span> <span class="n">l'</span>
<span class="k">end</span><span class="o">.</span>
<span class="kn">Lemma</span> <span class="n">multiplicity_app</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">nat</span><span class="o">)</span> <span class="o">(</span><span class="n">l1</span> <span class="n">l2</span> <span class="o">:</span> <span class="kt">list</span> <span class="n">nat</span><span class="o">)</span> <span class="o">:</span>
<span class="n">multiplicity</span> <span class="n">n</span> <span class="o">(</span><span class="n">l1</span> <span class="o">++</span> <span class="n">l2</span><span class="o">)</span> <span class="o">=</span> <span class="n">multiplicity</span> <span class="n">n</span> <span class="n">l1</span> <span class="o">+</span> <span class="n">multiplicity</span> <span class="n">n</span> <span class="n">l2</span><span class="o">.</span>
<span class="kn">Proof</span><span class="o">.</span>
<span class="k">induction</span> <span class="n">l1</span><span class="o">.</span> <span class="kp">reflexivity</span><span class="o">.</span>
<span class="k">simpl</span><span class="o">.</span> <span class="k">destruct</span> <span class="n">eq_nat_dec</span><span class="o">;</span> <span class="k">auto</span><span class="o">.</span>
<span class="k">rewrite</span> <span class="nn">IHl1</span><span class="p">.</span> <span class="n">auto</span><span class="o">.</span>
<span class="kn">Qed</span><span class="o">.</span></code></pre>
<p>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 <code>l'</code> est obtenue à partir de la liste <code>l</code> 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.</p>
<p>Voici deux preuves plus compliquées, reposant sur des définitions précédentes et bibliothèques de théorèmes. La <a href="http://www.cis.upenn.edu/%7Ebcpierce/sf/current/UseAuto.html#lab1008">première</a> énonce qu'un petit langage de programmation est déterministe : si le programme <code>c</code>, partant de l'état mémoire <code>st</code>, peut arriver soit dans l'état <code>st1</code> soit dans l'état <code>st2</code>, alors ces deux états sont égaux.</p>
<pre><code class="coq"><span class="kn">Theorem</span> <span class="n">ceval_deterministic</span><span class="o">:</span> <span class="err">∀</span><span class="n">c</span> <span class="n">st</span> <span class="n">st1</span> <span class="n">st2</span><span class="o">,</span>
<span class="n">c</span> <span class="o">/</span> <span class="n">st</span> <span class="err">⇓</span> <span class="n">st1</span> <span class="err">→</span>
<span class="n">c</span> <span class="o">/</span> <span class="n">st</span> <span class="err">⇓</span> <span class="n">st2</span> <span class="err">→</span>
<span class="n">st1</span> <span class="o">=</span> <span class="n">st2</span><span class="o">.</span>
<span class="kn">Proof</span><span class="o">.</span>
<span class="n">introv</span> <span class="nc">E1</span> <span class="nn">E2</span><span class="p">.</span> <span class="n">gen</span> <span class="n">st2</span><span class="o">.</span>
<span class="k">induction</span> <span class="nc">E1</span><span class="o">;</span> <span class="k">intros</span><span class="o">;</span> <span class="n">inverts</span><span class="err">×</span> <span class="nc">E2</span><span class="o">;</span> <span class="n">tryfalse</span><span class="o">.</span>
<span class="n">forwards</span><span class="o">*:</span> <span class="nn">IHE1_1</span><span class="p">.</span> <span class="n">subst</span><span class="err">×</span><span class="o">.</span>
<span class="n">forwards</span><span class="o">*:</span> <span class="nn">IHE1_1</span><span class="p">.</span> <span class="n">subst</span><span class="err">×</span><span class="o">.</span>
<span class="kn">Qed</span><span class="o">.</span></code></pre>
<p>La <a href="https://sympa.inria.fr/sympa/arc/ssreflect/2014-04/msg00001.html">seconde</a> fait partie d'une preuve qu'il y a une infinité de nombres premiers : pour tout nombre entier <code>m</code>, on peut trouver un nombre entier premier <code>p</code> strictement supérieur à <code>m</code>. </p>
<pre><code class="coq"><span class="kn">Lemma</span> <span class="n">prime_inf</span> <span class="n">m</span> <span class="o">:</span> <span class="o">{</span><span class="n">p</span> <span class="o">|</span> <span class="n">m</span> <span class="o"><</span> <span class="n">p</span> <span class="o">&</span> <span class="n">prime</span> <span class="n">p</span><span class="o">}.</span>
<span class="kn">Proof</span><span class="o">.</span>
<span class="k">pose</span> <span class="n">c</span> <span class="o">:=</span> <span class="n">pdiv</span> <span class="n">m</span><span class="o">`!.+</span><span class="mi">1</span><span class="o">.</span>
<span class="k">have</span> <span class="nc">Pc</span> <span class="o">:</span> <span class="n">prime</span> <span class="n">c</span> <span class="kp">by</span> <span class="k">apply</span><span class="o">/</span><span class="n">pdiv_prime</span><span class="o">/</span><span class="n">fact_gt0</span><span class="o">.</span>
<span class="k">exists</span> <span class="n">c</span> <span class="o">=></span> <span class="o">//.</span>
<span class="k">have</span> <span class="o">[</span><span class="n">cLm</span><span class="o">|//]</span> <span class="o">:=</span> <span class="n">leqP</span><span class="o">.</span>
<span class="k">have</span> <span class="o">/</span><span class="nc">Euclid_dvd1</span> <span class="o">:=</span> <span class="nn">Pc</span><span class="p">.</span>
<span class="n">have</span> <span class="o">/</span><span class="n">eqP</span><span class="o"><-</span> <span class="o">:=</span> <span class="n">coprimenS</span> <span class="o">(</span><span class="n">m</span><span class="o">`!).</span>
<span class="k">rewrite</span> <span class="n">dvdn_gcd</span> <span class="n">pdiv_dvd</span><span class="o">.</span>
<span class="kp">by</span> <span class="k">have</span> <span class="o">/</span><span class="n">fact_div</span><span class="o">-></span> <span class="o">:</span> <span class="mi">0</span> <span class="o"><</span> <span class="n">pdiv</span> <span class="n">m</span><span class="o">`!.+</span><span class="mi">1</span> <span class="o"><=</span> <span class="n">m</span> <span class="kp">by</span> <span class="k">rewrite</span> <span class="n">prime_gt0</span><span class="o">.</span>
<span class="kn">Qed</span><span class="o">.</span></code></pre>
<h3 id="Écosystème">Écosystème</h3>
<p>À 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 :</p>
<ul>
<li>
<a href="http://www.cs.utexas.edu/users/moore/acl2/">ACL2</a> ;</li>
<li>
<a href="http://pvs.csl.sri.com/">PVS</a> ;</li>
<li>La famille HOL (<a href="http://hol.sourceforge.net/">HOL4</a>, <a href="http://www.cl.cam.ac.uk/%7Ejrh13/hol-light/">HOL Light</a>…) ;</li>
<li>
<a href="http://isabelle.in.tum.de/">Isabelle</a>, successeur de HOL ;</li>
<li>
<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php">Agda</a>, qui est probablement l'un des plus proches cousins de Coq à l'état naturel.</li>
</ul><p>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 :</p>
<ul>
<li>Le projet <a href="https://code.google.com/p/flyspeck/">Flyspeck</a>, en HOL Light sous licence BSD, qui visait à prouver la <a href="https://fr.wikipedia.org/wiki/conjecture%20de%20Kepler" title="Définition Wikipédia">conjecture de Kepler</a>, 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 ! </li>
<li>Le système d'exploitation <a href="http://sel4.systems/">seL4</a> prouvé de bout en bout en Isabelle (et open sourcé GPL / BSD, de surcroît).</li>
</ul><p>Parmi les gros développements en Coq, on peut citer :</p>
<ul>
<li>Le <a href="https://fr.wikipedia.org/wiki/th%C3%A9or%C3%A8me%20des%20quatre%20couleurs" title="Définition Wikipédia">théorème des quatre couleurs</a>, prouvé en 2008 (45 kloc, licence non-spécifiée, <a href="https://github.com/kik/Four-Color-Theorem-Maintenance">code source</a>) ;</li>
<li>Le <a href="https://fr.wikipedia.org/wiki/th%C3%A9or%C3%A8me%20de%20Feit%20et%20Thompson" title="Définition Wikipédia">théorème de Feit et Thompson</a>, prouvé en 2012 (170 kloc, CECILL-B, <a href="https://gforge.inria.fr/projects/coqfinitgroup/">code source</a>) ;</li>
<li>
<a href="http://compcert.inria.fr/">CompCert</a>, un compilateur C certifié (110 kloc, hélas, une partie du <a href="https://github.com/AbsInt/CompCert">code source</a> est réservé aux utilisations non-commerciales uniquement) ;</li>
<li>
<a href="http://plv.csail.mit.edu/bedrock/">Bedrock</a>, un cadriciel de preuve de programmes (BSD, <a href="http://plv.csail.mit.edu/bedrock/bedrock-20140722.tgz">code source</a>).</li>
</ul><p>Il faut savoir que les deux premiers théorèmes ont été prouvés par <a href="https://fr.wikipedia.org/wiki/Georges%20Gonthier" title="Définition Wikipédia">Georges Gonthier</a> et son équipe, après une quantité impressionnante de travail acharné (6 ans pour Feit-Thompson).</p>
<h3 id="usage-industriel">Usage industriel</h3>
<p>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 <em>model checking</em> qui sont les plus automatisés et donc les plus faciles à utiliser (voir par exemple l'article <a href="http://www.cl.cam.ac.uk/%7Ejrh13/papers/ab.pdf"><em>A short survey of automated reasoning</em></a> de <a href="http://www.cl.cam.ac.uk/%7Ejrh13/">John Harrison</a>, 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.</p>
<p>Les assistants de preuves ont longtemps été réservés à un usage par une petite poignée d'experts (utilisation de la <a href="http://fr.wikipedia.org/wiki/M%C3%A9thode_B">méthode B</a> 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 <a href="http://ssrg.nicta.com.au/projects/TS/SMACCM/">été utilisé</a> 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…).</p>
<h2 id="quelques-nouveautés-de-coq-85">Quelques nouveautés de Coq 8.5</h2>
<p>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.</p>
<ul>
<li>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)</li>
<li>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)</li>
<li>un nouveau mécanisme d'évaluation des termes, <code>native_compute</code> 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)</li>
<li>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)</li>
</ul><p>Quelques autres changements importants sont:</p>
<ul>
<li>Une construction <code>$(...)$</code> qui permet d'intégrer des bouts de tactique directement dans des programmes — on ne pouvait auparavant faire que l'inverse avec la tactice <code>refine</code>. C'est très très pratique.</li>
<li>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'<a href="https://fr.wikipedia.org/wiki/Axiome_d%27extensionnalit%C3%A9">extensionnalité</a> des propositions, et des conséquences de l'univalence).</li>
<li>Une nouvelle option <code>-type-in-type</code> qui rend la logique incohérente (on peut prouver <code>False</code>) mais est pratique pour prototyper des idées sans avoir à gérer les niveau d'univers dans un premier temps.</li>
<li>Une tactique <code>cbn</code> qui remplace avantagement <code>simpl</code>.</li>
<li>Un nouveau motif introductif <code>= x1 .. xn</code> qui applique <code>injection</code> au vol (inspiré de <a href="http://ssr.msr-inria.inria.fr/">SSReflect</a>, un jeu alternatif de tactiques de base pour Coq)</li>
<li>De nouvelles constructions <code>uconstr:c</code> et <code>type_term c</code> pour programmer des tactiques manipulant des termes pas encore typés. </li>
</ul><p>Le <a href="https://github.com/coq/coq/blob/v8.5/CHANGES">Changelog complet</a> est disponible. La partie cachée de l'iceberg contient de nombreuses modifications et <em>bugfixes</em> (avec en particulier Pierre Boutillier, Hugo Herbelin, Pierre Letouzey et Pierre-Marie Pédrot).</p>
<h2 id="preuves-et-programmes--deux-faces-de-la-même-pièce">Preuves et programmes : deux faces de la même pièce</h2>
<p><em>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.</em></p>
<p>Coq possède une particularité que ne présentent pas la majorité des autres assistants de preuve : il est basé sur la fameuse <a href="https://fr.wikipedia.org/wiki/correspondance%20de%20Curry-Howard" title="Définition Wikipédia">correspondance de Curry-Howard</a>. 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[<sup>1]</sup> !</p>
<h3 id="un-peu-dhistoire">Un peu d'histoire</h3>
<p>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.</p>
<p>À 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 λόγος (<em>logos</em>) signifiant « parole ».</p>
<p>Ce nommé Aristote écrit l'<em>Organon</em>, qui deviendra jusqu'au XIXe siècle à la logique ce que <em>The C Programming Language</em> est au langage C. On y apprend des choses fort intéressantes, dont voici un exemple afin d'en jauger la teneur :</p>
<ul>
<li>Socrate est un homme.</li>
<li>Tous les hommes sont mortels.</li>
<li>Donc Socrate est mortel.</li>
</ul><p>Si l'<em>Organon</em> a fait le délice des étudiants en scolastique médiévaux, il faut attendre la fin du XIX<sup>è</sup> 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.</p>
<h3 id="les-grands-ancêtres">Les grands ancêtres</h3>
<p>Le début du XXe siècle est une période fertile pour les progrès de la logique formelle[<sup>2].</sup> 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 <a href="https://fr.wikipedia.org/wiki/paradoxe%20de%20Russell" title="Définition Wikipédia">paradoxe de Russell</a>, 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.</p>
<p>À 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.</p>
<ul>
<li>Les <a href="https://fr.wikipedia.org/wiki/Machine_de_Turing">machines de Turing</a>, inventées par <a href="https://fr.wikipedia.org/wiki/Alan%20Turing" title="Définition Wikipédia">Alan Turing</a> en 1936.</li>
<li>Le <a href="https://fr.wikipedia.org/wiki/Lambda-calcul">λ-calcul</a>, dû à <a href="https://fr.wikipedia.org/wiki/Alonzo%20Church" title="Définition Wikipédia">Alonzo Church</a>, daté des années 30.</li>
</ul><p>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.</p>
<h3 id="des-systèmes-de-types-aux-systèmes-de-preuves">Des systèmes de types aux systèmes de preuves</h3>
<p>Les premiers langages fonctionnels comme <a href="https://fr.wikipedia.org/wiki/LISP" title="Définition Wikipédia">LISP</a> 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 <a href="https://fr.wikipedia.org/wiki/ML_(langage)">ML</a> 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, <a href="http://en.wikipedia.org/wiki/Logic_for_Computable_Functions">LCF</a>, 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.</p>
<p>La correspondance de Curry-Howard est la découverte fortuite par <a href="https://fr.wikipedia.org/wiki/Haskell%20Curry" title="Définition Wikipédia">Haskell Curry</a> en 1958 puis <a href="https://fr.wikipedia.org/wiki/William%20Alvin%20Howard" title="Définition Wikipédia">William Alvin Howard</a> en 1969 que le système de types primitif du λ-calcul correspondait en fait <em>exactement</em> à un système logique minimaliste, la bien nommée <em>logique propositionnelle minimale</em>. C'était là la découverte d'une véritable <strong>pierre de Rosette</strong> 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).</p>
<p>La correspondance de Curry-Howard énonce ainsi que :</p>
<ul>
<li>Les preuves mathématiques sont les programmes des langages fonctionnels ;</li>
<li>Les formules logiques que démontrent ces preuves sont les types de ces programmes.</li>
</ul><p>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.</p>
<table>
<thead><tr>
<th>Informatique</th>
<th>Mathématiques</th>
</tr></thead>
<tbody>
<tr>
<td>Type</td>
<td>Formule</td>
</tr>
<tr>
<td>Programme</td>
<td>Preuve</td>
</tr>
<tr>
<td>Primitive système</td>
<td>Axiome</td>
</tr>
<tr>
<td>Fonction de <em>A</em> vers <em>B</em>
</td>
<td>Preuve de « <em>A</em> implique <em>B</em> »</td>
</tr>
<tr>
<td>Paire de <em>A</em> et <em>B</em>
</td>
<td>Preuve de « <em>A</em> et <em>B</em> »</td>
</tr>
<tr>
<td>Type somme sur <em>A</em> et <em>B</em>
</td>
<td>Preuve de « <em>A</em> ou <em>B</em> »</td>
</tr>
<tr>
<td>Interpréteur</td>
<td><a href="https://fr.wikipedia.org/wiki/Correction_(logique)">Théorème de correction</a></td>
</tr>
<tr>
<td>Décompilateur</td>
<td><a href="https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me%20de%20compl%C3%A9tude" title="Définition Wikipédia">Théorème de complétude</a></td>
</tr>
</tbody>
</table><p>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.</p>
<h3 id="de-nouvelles-fondations">De nouvelles fondations</h3>
<p>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 <a href="https://fr.wikipedia.org/wiki/Thierry%20Coquand" title="Définition Wikipédia">Thierry Coquand</a> à la fin des années 1980. Il convient de citer aussi la théorie des types de <a href="https://fr.wikipedia.org/wiki/Per_Martin-L%C3%B6f">Martin-Löf</a> (MLTT), qui lui est similaire, sur laquelle se base Agda.</p>
<p>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.</p>
<p>Tout récemment, le petit monde de la théorie de la démonstration a été secoué par les idées de <a href="https://fr.wikipedia.org/wiki/Vladimir%20Vo%C3%AFevodski" title="Définition Wikipédia">Vladimir Voïevodski</a>, 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 <a href="http://homotopytypetheory.org/book/">HoTT Book</a>[<sup>4].</sup></p>
<h3 id="méli-mélo-de-coq-au-curry-howard">Méli-mélo de Coq au Curry-Howard</h3>
<p>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 :</p>
<pre><code class="coq"><span class="kn">Definition</span> <span class="n">pred</span> <span class="o">:</span> <span class="k">forall</span> <span class="n">n</span> <span class="o">:</span> <span class="n">nat</span><span class="o">,</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">nat</span> <span class="o">|</span> <span class="n">n</span> <span class="o">=</span> <span class="mi">0</span> <span class="o">\/</span> <span class="n">n</span> <span class="o">=</span> <span class="nc">S</span> <span class="n">m</span><span class="o">}</span> <span class="o">:=</span>
<span class="k">fun</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">nat</span><span class="o">)</span> <span class="o">=></span>
<span class="c">(** analyse de cas sur n *)</span>
<span class="k">match</span> <span class="n">n</span> <span class="k">return</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">nat</span> <span class="o">|</span> <span class="n">n</span> <span class="o">=</span> <span class="mi">0</span> <span class="o">\/</span> <span class="n">n</span> <span class="o">=</span> <span class="nc">S</span> <span class="n">m</span><span class="o">}</span> <span class="k">with</span>
<span class="c">(** n vaut zéro *)</span>
<span class="o">|</span> <span class="mi">0</span> <span class="o">=></span> <span class="n">exist</span> <span class="o">_</span> <span class="mi">0</span> <span class="o">(</span><span class="n">or_introl</span> <span class="n">eq_refl</span><span class="o">)</span>
<span class="c">(** n est de la forme n' + 1 *)</span>
<span class="o">|</span> <span class="nc">S</span> <span class="n">n'</span> <span class="o">=></span> <span class="n">exist</span> <span class="o">_</span> <span class="n">n'</span> <span class="o">(</span><span class="n">or_intror</span> <span class="n">eq_refl</span><span class="o">)</span>
<span class="k">end</span><span class="o">.</span></code></pre>
<p>Ce fragment se lit ainsi :</p>
<ul>
<li>Version informatique : on définit la fonction <code>pred</code> qui prend en argument un entier naturel <code>n</code> et qui renvoie un entier naturel <code>m</code> tel que soit <code>n</code> vaut zéro, soit <code>n = m + 1</code>.</li>
<li>Version mathématique : le théorème <code>pred</code> affirme que pour tout entier naturel <code>n</code>, il existe un entier naturel <code>m</code> tel que <code>n</code> vaut zéro ou <code>n = m + 1</code>.</li>
</ul><p>Et effectivement, on peut calculer le résultat de l'application de cette fonction-théorème (<code>proj1_sig</code> est la fonction qui extrait le témoin de l'existentielle).</p>
<pre><code class="coq"><span class="nc">Eval</span> <span class="k">compute</span> <span class="k">in</span> <span class="n">proj1_sig</span> <span class="o">(</span><span class="n">pred</span> <span class="mi">42</span><span class="o">).</span>
<span class="o">=</span> <span class="mi">41</span>
<span class="o">:</span> <span class="n">nat</span></code></pre>
<p>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.</p>
<pre><code class="coq"><span class="kn">Definition</span> <span class="n">pred</span> <span class="o">:</span> <span class="k">forall</span> <span class="n">n</span> <span class="o">:</span> <span class="n">nat</span><span class="o">,</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">nat</span> <span class="o">|</span> <span class="n">n</span> <span class="o">=</span> <span class="mi">0</span> <span class="o">\/</span> <span class="n">n</span> <span class="o">=</span> <span class="nc">S</span> <span class="n">m</span><span class="o">}.</span>
<span class="kn">Proof</span><span class="o">.</span>
<span class="k">intros</span> <span class="n">n</span><span class="o">;</span> <span class="k">destruct</span> <span class="n">n</span><span class="o">.</span>
<span class="o">+</span> <span class="k">exists</span> <span class="mi">0</span><span class="o">;</span> <span class="k">left</span><span class="o">;</span> <span class="kp">reflexivity</span><span class="o">.</span>
<span class="o">+</span> <span class="k">exists</span> <span class="n">n</span><span class="o">;</span> <span class="k">right</span><span class="o">;</span> <span class="kp">reflexivity</span><span class="o">.</span>
<span class="kn">Defined</span><span class="o">.</span></code></pre>
<p>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.</p>
<p>Agda, le seul autre assistant de preuve <em>mainstream</em> 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.)</p>
<h3 id="un-langage-exotique">Un langage exotique</h3>
<p>En tant que langage de programmation, Coq fait malgré tout figure d'alien aux yeux des programmeurs lambda.</p>
<p>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 <em>Hello World</em> 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 <a href="https://fr.wikipedia.org/wiki/monade" title="Définition Wikipédia">monade</a>, comme en Haskell.</p>
<p>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 ».</p>
<p>Une conséquence inattendue de ce fait : Coq n'est <strong>pas</strong> Turing-complet. Il existe donc des programmes qu'on ne peut pas écrire en Coq. Ce n'est pas un <em>bug</em>, c'est une <em>feature</em> ! Cette restriction permet de passer outre les limitations dues au <a href="https://fr.wikipedia.org/wiki/th%C3%A9or%C3%A8me%20d'incompl%C3%A9tude%20de%20G%C3%B6del" title="Définition Wikipédia">théorème d'incomplétude de Gödel</a> — mais complique l'écriture de programme dont on ne sait pas prouver la terminaison ou la productivité<sup>[3].</sup></p>
<h2 id="le-futur">Le futur ?</h2>
<p>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.</p>
<p>Des bibliothèques importantes de mathématiques formalisées existent déjà (par exemple le journal <a href="http://fm.mizar.org/">Formalized Mathematics</a> 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.</p>
<p>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.</p>
<p>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, <em>runtime</em>, 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.</p>
<p>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.</p>
<h3 id="notes">Notes</h3>
<p><sup>[0]</sup> 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 <a href="http://gallium.inria.fr/%7Efpottier/publis/fpottier-dfs-scc.pdf">remarquables</a>, 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 <em>Comment prouver formellement X</em> que vous trouverez l'exposition la plus claire du sujet X.</p>
<p><sup>[1]</sup> Peut-être presque autant que la sortie de l'iPhone <em>n + 1</em>, pour un <em>n</em> bien choisi.</p>
<p><sup>[2]</sup> Je recommande la lecture de la captivante BD <a href="https://fr.wikipedia.org/wiki/Logicomix" title="Définition Wikipédia">Logicomix</a> à ceux qui sont intéressés.</p>
<p><sup>[3]</sup> 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 <em>bootstrapper</em> à l'aide d'un axiome bien choisi.</p>
<p><sup>[4]</sup><a href="http://math.andrej.com/2013/06/20/the-hott-book/">Quand un mathématicien déclare son amour à git et à l'esprit du libre</a>.</p></div><div><a href="https://linuxfr.org/news/sortie-de-coq-8-5-beta-un-assistant-de-preuve-formelle.epub">Télécharger ce contenu au format EPUB</a></div> <p>
<strong>Commentaires :</strong>
<a href="//linuxfr.org/nodes/104498/comments.atom">voir le flux Atom</a>
<a href="https://linuxfr.org/news/sortie-de-coq-8-5-beta-un-assistant-de-preuve-formelle#comments">ouvrir dans le navigateur</a>
</p>
PerthmâdgascheBAudanasetoZeroHeureSnarkYves Bourguignonpalm123renoNicolas BoulayNils RatusznikOntologiahttps://linuxfr.org/nodes/104498/comments.atom