1.2. Guide de lecture
Quatre mots ont ici un sens fixe et ne s'emploient pas l'un pour l'autre. Les énoncés qui suivent sont de forces très inégales, et c'est à ces mots qu'on les reconnaît. Un postulat est posé et non dérivé : les quatre du chapitre 1 sont de cette espèce, et ils servent de filtre d'évaluation plutôt que de nomenclature. Un théorème est démontré ou esquissé, dans un environnement nommé, sa réserve écrite dans l'esquisse. Un engagement est tenu pour vrai sans démonstration, et le dit ; la liste en est donnée ci-dessous, exhaustive et courte. Une lecture est une analogie organisatrice, sans force démonstrative : le mot sert quand une structure éclaire sans engager.
Trois mots complètent ces quatre, que ce document emploie constamment et qu'il serait malhonnête de laisser hors de la convention. Une réserve borne la portée d'un résultat, pour empêcher qu'on lui prête plus qu'il n'établit. Une obligation est une preuve à fournir au vérificateur, portée par un terme et non par le document. Une exigence est une contrainte que l'implémentation doit satisfaire, et dont ni la démonstration ni la réfutation n'appartiennent à ce texte.
Cette convention a une conséquence que le lecteur peut exiger : là où aucun de ces sept mots n'apparaît, l'énoncé est une conséquence de ce qui précède, et le renvoi qui l'accompagne dit d'où il vient.
Il y a onze engagements, et leur brièveté est en soi une donnée : la plupart de ce qui en fut un au cours de la rédaction est devenu soit un théorème, soit une réserve explicite.
Les onze engagements, ce qu'ils affirment, ce qui les tient et par où ils se lèveront
Engagement | Où | Ce qui le tient | Route |
|---|---|---|---|
La cohérence au sens de Kelly et Mac Lane | §2.2 | La littérature primaire le référence sans le redémontrer | littérature |
L'enrichissement sur les préordres, pour la part qui excède l'ordre des fibres | §2.4 | Rien ; le théorème 12 en dérive l'autre part | démonstration |
L'isolation par types plutôt que par unité de gestion mémoire | §4.5 | Une réalisation déployée, non une preuve | mesure |
La conformité de l'abaissement au modèle mémoire déclaré | §4.5 | Rien ; c'est une propriété du compilateur | démonstration |
La fidélité de l'interpréteur de référence | §6.3 | Le théorème 45, dont l'induction est planifiée au §4.7.6 mais non conduite, et l'hypothèse Sim du théorème 47, à établir | démonstration (rouverte : Sim) |
Le coût d'expressivité de P3 et P4, inférieur au bénéfice | §1.3 | Un pari, dont le protocole de mesure est écrit et non conduit | mesure |
La reproductibilité de la compilation | §5.5 | Visée, non garantie — et le document l'écrit | mesure |
La rareté des changements de fragment, qui borne la verbosité des délimiteurs | §5.1 | Un pari, mesurable dès le gel de la syntaxe et non encore mesuré | mesure |
La correction de ressource — le grade tient ce qu'il annonce | §4.7 | Rien ; l'énoncé est posé, sa preuve reste à conduire | démonstration |
L'accord entre la réduction et son interprétation | §2.1 | Rien ; c'est ce qui relierait la machine au modèle | démonstration |
L'existence de l'interprétation | §2.1 | Rien ; le premier postulat la suppose sans la construire | démonstration |
Aucun de ces engagements n'est caché : chacun est signalé là où il est pris, et la table 1 ne fait que les rassembler. Ils ne sont pas de même nature. Les deux paris sur l'usage — le coût d'expressivité des deux postulats, et la rareté des changements de fragment — ne se tranchent que par une mise à l'épreuve, et ce document écrit désormais laquelle plutôt que de la laisser à imaginer. Le second se mesure sur du texte, sans rien exécuter : on écrit un corpus de programmes représentatifs, on compte les franchissements de fragment par millier de lignes, et on rapporte ce nombre à celui des expressions. La mesure est disponible dès que la syntaxe est gelée, et elle n'attend aucun prototype. Le premier demande le noyau exécutable : on relève les programmes du corpus que les deux postulats rejettent, et l'on regarde pour chacun s'il existe une reformulation acceptée — ce qui rend un taux de rejet sans reformulation disponible, et non une opinion. Écrire ces deux protocoles ne les acquitte pas ; cela dit ce qu'un pair devrait refaire pour les contredire. Les autres sont des propositions dont on saurait dire ce qu'il faudrait pour les établir.
Une règle gouverne désormais cette table, et elle vaut d'être posée parce qu'un engagement qui ne dit pas comment il se lèvera n'est pas un engagement mais un aveu. RMQ 2. Trois routes seulement. Une quatrième — « on verra » — n'en est pas une. Tout engagement de ce document nomme la route par laquelle il se lèvera, et il n'y en a que trois. La littérature : l'énoncé est déjà établi ailleurs, et il suffit de le référencer dans sa source primaire plutôt que de le redémontrer. La démonstration : il ne l'est pas, et ce document ou sa mécanisation doit le prouver — auquel cas l'engagement porte le nom du théorème qui l'acquittera. La mesure : il ne se démontre pas du tout, étant un énoncé sur l'usage ou sur une réalisation, et l'engagement porte alors le protocole qui le trancherait.
Trois conséquences suivent, et la première a déjà joué. Un engagement dont la route est la démonstration cesse d'être un engagement le jour où le théorème est écrit : la fidélité de l'interpréteur de référence en était sortie, la section sur la traduction passant pour avoir démontré que celle-ci préserve le typage ; elle y est rentrée, l'induction étant planifiée et non conduite. La table le dit maintenant — un document qui ne relit pas ses engagements finit par s'accuser de dettes qu'il a payées, ou par se croire quitte de celles qu'il n'a pas payées. La deuxième est qu'un engagement dont la route est la mesure ne se lèvera jamais par la lecture, et qu'il est vain de l'y attendre. La troisième est qu'un engagement sans route nommée est une anomalie : il en reste un dans cette table, l'enrichissement sur les préordres pour la part qui excède l'ordre des fibres, et sa route est la démonstration — le théorème 12 en dérive l'autre part, et rien n'établit encore celle-là.
Une lecture est une analogie qui organise sans engager. Il n'en reste que deux, et c'est le résultat d'un travail. La plupart des analogies de la première rédaction ont été soit démontrées — le namespace comme inclusion fonctorielle, l'orchestrateur comme coalgèbre, le grade de présence comme fragment affine — soit requalifiées en réserve.
La sédimentation triadique est une lecture : que les trois couches se « déposent » l'une sur l'autre est une image, et ce qui la soutient formellement est l'inclusion des fragments, qui est autre chose. Cette réserve a désormais une mesure : l'inclusion tient sur l'axe des ressources et s'inverse sur deux autres. Sur celui des effets, où la couche 3 est la plus pauvre puisqu'elle n'en a aucun ; et sur celui de la concurrence, où elle est la plus pauvre également, son parallélisme étant déterministe quand la couche 2 porte l'entrelacement (§3.6.4.4). Une image qui ne vaut que sur un axe doit dire lequel. La couche 2 comme langage de liaison, au sens d'Ousterhout, en est une seconde : elle situe le rôle sans rien en dériver.
Un dernier choix précède tous les autres, et il est écrit ici parce que la question serait sinon reposée à chaque relecture : le socle de K7PL est une famille modale et graduée, non un socle homotopique. Quatre motifs, dont trois sont de fond. L'univalence rend inexprimable ce que K7PL doit prouver : tout énoncé y est invariant par équivalence, quand les énoncés de représentation et de rejeu affirment que deux représentations équivalentes coïncident, ou non, bit à bit. Le transport a un coût, que le postulat d'autonomie physique interdit de dissimuler et qu'aucune théorie publiée ne compte dans un budget. L'assistant de preuve visé impose l'irrélevance définitionnelle des preuves, ce qui contredit l'univalence. Enfin aucune variante homotopique ne fournit le semi-anneau ordonné agissant sur le contexte, qui est le cœur de K7PL. Ce choix n'exclut pas les imports ciblés d'une même famille — théorie de modes pour ranger les modalités, calf pour le coût et la distinction de phase, théorie des types graduée formalisée pour l'effacement et la décidabilité, récursion gardée pour la productivité —, qui s'instruisent un à un et ne sont versés au texte qu'au fur et à mesure qu'ils le sont ; ni l'emploi ponctuel et instrumental, comme outil de preuve, d'une théorie cubique sans types de Glue pour la seule dette de la sédimentation graduée.