Votre première preuve

dix minutes · trois étapes · rien que vous ayez à croire sur parole

Ceci est le parcours débutant. Vous n'avez pas besoin d'être programmeur, vous n'avez pas besoin de compte, et vous n'avez pas besoin de nous dire que vous existez. À la fin, votre propre ordinateur — pas le nôtre, et pas notre parole pour le garantir — aura vérifié les mathématiques derrière une véritable règle de la bibliothèque.

Si vous savez déjà vous repérer avec un prouveur, le parcours complet va plus loin : construire le front et vérifier chaque ligne de sa table de vérité. Cette page s'arrête à la preuve, qui est la partie la plus importante et celle qui ne nécessite rien d'installé.

Ce que vous allez vérifier

La règle s'appelle brief-fill policy. Elle décide quand un assistant peut répondre au nom de son propriétaire plutôt que de le lui demander. Quatre affirmations sont faites à son sujet, et les quatre s'apprêtent à être testées sur votre machine :

• elle ne remplit jamais une réponse sans une règle qui l'autorise ;
• si le dépôt de règles est absent, rien ne passe ;
• elle n'invente jamais rien ;
• elle ne vous demande jamais quelque chose qu'une règle a déjà tranché.

Ce ne sont pas des promesses dans un billet de blog. Ce sont des théorèmes, et un prouveur s'apprête à essayer de les briser.

Étape 1 — procurez-vous le prouveur

Il est gratuit et il n'est pas à nous — il vient de la communauté Ada, pas de nous. C'est bien là le sens : la chose qui vérifie notre travail ne devrait pas être une chose que nous vous avons remise.

Étape 2 — procurez-vous la règle

Vous pouvez ignorer la somme de contrôle lors d'un premier essai — la preuve de l'étape 3 n'en dépend pas. Elle est là pour le jour où vous voudrez confirmer que le fichier reçu est bien celui que nous avons publié, et c'est le même que nomme le catalogue.

Étape 3 — demandez à votre ordinateur de la vérifier

Ouvrez un terminal dans le dossier décompressé et lancez deux lignes :

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2

Attendez. Quand cela se termine, cherchez ces deux mots :

0 unproved

C'est tout. C'est tout l'exercice. Rien d'autre n'a besoin d'être installé, et cette étape fonctionne sur une machine nue, sans rien d'autre dessus — le prouveur que vous avez téléchargé porte tout ce dont la preuve a besoin.

Ce qui vient de se passer

Votre ordinateur a pris les quatre affirmations ci-dessus, a essayé de trouver un cas où l'une d'elles échoue, et n'a pas pu — parce qu'il n'en existe pas. Pas « nous l'avons testé et cela semblait aller ». Pas « le mainteneur le dit ». Une machine que l'on ne peut pas amadouer est partie à la recherche d'un contre-exemple et est revenue bredouille.

Vous ne nous avez pas fait confiance pour vous le dire. Vous l'avez vu se produire sur du matériel qui vous appartient.

Facultatif — cassez-la exprès

C'est la partie qui vaut la peine si vous avez cinq minutes de plus, parce qu'une vérification qui ne dit jamais que oui ne vaut pas grand-chose.

Ouvrez brief_fill_policy_pkg.ads dans n'importe quel éditeur de texte et modifiez la règle pour qu'un dépôt manquant laisse quand même passer une réponse. Relancez la même commande. Elle refusera — et elle nommera le théorème exact que vous venez de briser.

Ce refus est tout le modèle de sécurité. Ghillie n'installe rien qui ne passe pas cette épreuve, si bien que ce que vous venez de faire à la main est ce qu'il fait en votre nom à chaque fois.

Ce que cela ne prouve pas

Nous préférons vous le dire plutôt que vous le découvriez plus tard. Les preuves couvrent les règles de décision — qui peut voir quoi, ce qui peut sortir, ce qu'une livraison doit satisfaire. Elles ne rendent pas le reste du logiciel magique, et nous ne prétendons pas le contraire. Cette honnêteté est le contrat, et c'est tout le contrat.

Où aller ensuite

• Le parcours complet — construire le front et vérifier chaque ligne de sa table de vérité fournie.
• Le catalogue — le reste de l'étagère, chaque pièce re-dérivable de la même façon.
• Ghillie — l'assistant que ces règles servent.
• La machine du Récif — quel matériel il vous faut si vous voulez aller plus loin que cette page.

Si cela n'a pas fonctionné, c'est un constat et nous aimerions le connaître. Un refus que vous ne pouvez pas expliquer nous intéresse plus qu'une réussite.