Résumé

  • Dans Edinburgh LCF, une tactique transforme un but en sous-buts et remet une fonction de validation. Ce n’est qu’en recombinant des théorèmes de sous-buts au moyen des règles primitives que le résultat devient un théorème.
  • Le type abstrait thm réduit la surface directement investie du pouvoir de construction. Il ne démontre ni la cohérence de la logique, ni l’adéquation de la spécification au réel, ni l’absence de défauts dans le compilateur, l’exécution ou le matériel.
  • Le mérite est collectif : la logique vient de Dana Scott, Stanford LCF précède le système d’Édimbourg, et Michael Gordon, Christopher Wadsworth, Lockwood Morris, Malcolm Newey ainsi que d’autres chercheurs ont participé à LCF et ML.

Une réussite de recherche n’est pas encore une admission

Partons d’un but. Un programme essaie des réécritures, recule, enchaîne plusieurs méthodes puis déclare les sous-buts résolus. Un journal d’exécution peut rendre cette histoire très convaincante. LCF impose pourtant une question plus stricte : la procédure peut-elle produire le théorème demandé par la seule interface autorisée ?

La tactique ne reçoit pas un droit spécial sur les théorèmes. Elle fournit des sous-buts et une validation, c’est-à-dire une fonction qui prendra les théorèmes correspondant à ces sous-buts et construira le théorème du but initial. Si cette fonction échoue ou ne livre pas la conclusion promise, la belle trajectoire de recherche ne vaut rien comme preuve admise.

Cette séparation répondait à une tension concrète. Un assistant interactif doit permettre à ses utilisateurs d’inventer des méthodes. Leur code sera parfois mauvais. Si chaque extension pouvait fabriquer librement un objet « théorème », la confiance requise grandirait avec l’écosystème. Edinburgh LCF plaçait donc les théorèmes derrière un type abstrait, traditionnellement appelé thm. Les opérations capables d’en produire étaient les axiomes et les règles d’inférence du calcul.

Le système ne promettait pas l’infaillibilité des tactiques. Une tactique peut diverger, choisir une mauvaise décomposition, déclencher une exception ou retourner une validation inutilisable. La propriété utile est plus modeste : l’erreur située hors de l’interface ne donne pas naissance à un constructeur clandestin. Elle se manifeste normalement par l’absence du théorème attendu.

Une histoire d’équipe, pas une signature solitaire

En 1972, Milner présentait un vérificateur pour la Logic for Computable Functions de Dana Scott. Cette phase à Stanford montra la possibilité d’une mécanisation, mais aussi le coût des longues preuves manipulées à bas niveau. Après son arrivée à Édimbourg en 1973, le projet chercha une forme plus programmable.

Le livre de référence de 1979 porte les noms de Michael J. C. Gordon, Robin Milner et Christopher P. Wadsworth. L’article de 1978 sur le métalangage ajoute Lockwood Morris et Malcolm Newey. Les rétrospectives de Larry Paulson et Michael Gordon décrivent la continuité entre Stanford LCF, Edinburgh LCF, Cambridge LCF, HOL et Isabelle. Attribuer à Milner une intuition architecturale majeure n’autorise donc pas à lui attribuer seul ML, les tactiques ou la preuve interactive.

ML signifiait d’abord « Meta Language ». Il servait à programmer les procédures de preuve. Sa discipline de types polymorphes devint ensuite une contribution autonome ; le texte de Milner de 1978 formule notamment des résultats de sûreté sémantique et syntaxique et décrit un algorithme de typage déjà utilisé dans Edinburgh LCF. L’ACM a reconnu LCF, ML et CCS dans la citation du prix Turing de 1991, mais cette distinction n’efface pas la production collective.

Dans ce dispositif, la règle d’inférence travaille en avant, d’un ensemble de théorèmes vers un nouveau théorème. La tactique travaille en arrière, d’un but vers des sous-buts. La validation relie les deux directions. Les « tacticals » combinent les tactiques par séquence, répétition ou choix ; ils organisent la recherche, sans devenir pour autant de nouvelles règles primitives.

Ce que protège vraiment le type abstrait

Un type abstrait masque sa représentation et n’expose que certaines opérations. Le code utilisateur peut transporter une valeur thm et la fournir à une règle, mais pas éditer son contenu privé pour en forger une autre. La vérification des types maintient la barrière prévue.

Le bénéfice est une réduction de périmètre. On peut concentrer l’examen sur les axiomes et les implémentations des règles plutôt que sur chaque tactique. Un nouvel automatisme peut être complexe : son résultat reste obligé de revenir par le même passage. La quantité de code inventif cesse ainsi d’être égale à la quantité de code détenant directement l’autorité d’admission.

Mais « petit noyau » ne signifie pas « confiance nulle ». Une règle primitive mal conçue demeure dangereuse. Il faut encore croire que l’implémentation de ML respecte l’abstraction, que le compilateur et l’environnement d’exécution se comportent comme prévu et que la machine ne corrompt pas le calcul. Un analyseur ou un affichage peut aussi présenter autre chose que l’objet réellement établi. La base de confiance est comprimée, pas supprimée.

La sûreté du noyau n’est pas davantage synonyme de cohérence logique. Le fait qu’une valeur n’ait pu être construite que par certaines fonctions décrit sa provenance. Il ne prouve pas, à lui seul, que chacune de ces fonctions formalise une inférence valide. Et même une preuve impeccable ne démontre pas que la spécification décrit fidèlement le système réel : elle établit une conséquence du modèle choisi.

La validation, charnière discrète

La validation n’est pas un simple voyant vert. Elle transporte l’obligation différée de justifier la transformation du but. Supprimer graphiquement un objectif n’est pas le démontrer. Même une tactique qui ne retourne aucun sous-but doit fournir une validation capable de créer le théorème du but sans prémisse inventée.

Lorsque des tacticals composent plusieurs recherches, leurs validations doivent être composées elles aussi. Le contrôle peut donc devenir élaboré tout en conservant une chaîne qui revient aux règles primitives. C’est ce mécanisme qui sépare un récit d’activité — journal, script, message de succès — de l’objet admis.

Cette idée a marqué de nombreux assistants. Gordon l’a prolongée dans HOL ; Paulson a développé Cambridge LCF puis Isabelle. Cependant, Paulson souligne qu’Isabelle représente règles et états de preuve selon des principes différents du modèle classique. Les systèmes à termes de preuve, les vérificateurs de certificats et les assistants de type Coq organisent aussi leur confiance autrement. La filiation est réelle ; l’identité d’architecture ne l’est pas.

Sources et limites

Cette analyse historique ne constitue pas un audit d’un assistant actuel et ne mesure aucune taille de noyau. L’analogie avec une règle commune minimale, vérifiable localement et ouverte à des méthodes futures provient d’une lecture éditoriale du principe de spécification initiale minimale de Lu Heng ; elle ne décrit pas une position institutionnelle de Milner.