Ihr erster Beweis

zehn Minuten · drei Schritte · nichts, was Sie einfach glauben müssen

Das ist der Einsteigerpfad. Sie müssen kein Programmierer sein, Sie brauchen kein Konto, und Sie müssen uns nicht sagen, dass es Sie gibt. Am Ende davon wird Ihr eigener Rechner — nicht unserer, und nicht unser Wort dafür — die Mathematik hinter einer echten Regel aus der Bibliothek geprüft haben.

Wenn Sie sich mit einem Prover bereits auskennen, geht der vollständige Rundgang weiter: das Frontend bauen und jede Zeile seiner Wahrheitstafel prüfen. Diese Seite endet beim Beweis — dem Teil, der am wichtigsten ist, und dem Teil, der nichts Installiertes braucht.

Was Sie gleich prüfen

Die Regel heißt brief-fill policy. Sie legt fest, wann ein Assistent im Namen seines Eigentümers antworten darf, statt ihn zu fragen. Vier Behauptungen werden über sie aufgestellt, und alle vier werden gleich auf Ihrer Maschine geprüft:

• sie füllt nie eine Antwort aus ohne eine Regel, die es erlaubt;
• fehlt der Regelspeicher, kommt nichts durch;
• sie erfindet nie etwas;
• sie fragt Sie nie etwas, das eine Regel bereits beantwortet.

Das sind keine Versprechen in einem Blogeintrag. Das sind Theoreme, und gleich versucht ein Prover, sie zu brechen.

Schritt 1 — den Prover holen

Er ist kostenlos, und er ist nicht unserer — er kommt aus der Ada-Community, nicht von uns. Das ist der Punkt: Das, was unsere Arbeit prüft, sollte nicht etwas sein, das wir Ihnen in die Hand gedrückt haben.

Schritt 2 — die Regel holen

Beim ersten Durchlauf können Sie die Prüfsumme ignorieren — der Beweis in Schritt 3 hängt nicht von ihr ab. Sie ist da, falls Sie bestätigen wollen, dass die Datei, die Sie erhalten haben, die Datei ist, die wir veröffentlicht haben, und es ist dieselbe, die der Katalog nennt.

Schritt 3 — Ihren Rechner bitten, es zu prüfen

Öffnen Sie ein Terminal im entpackten Ordner und führen Sie zwei Zeilen aus:

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

Warten Sie. Wenn es fertig ist, halten Sie nach diesen beiden Wörtern Ausschau:

0 unproved

Das war's. Das ist die ganze Übung. Nichts weiter muss installiert werden, und dieser Schritt funktioniert auf einer nackten Maschine ohne sonst etwas darauf — der Prover, den Sie heruntergeladen haben, bringt alles mit, was der Beweis braucht.

Was gerade passiert ist

Ihr Rechner hat die vier obigen Behauptungen genommen, versucht, einen Fall zu finden, in dem eine von ihnen versagt, und konnte keinen finden — weil es keinen gibt. Nicht „wir haben es getestet, und es schien in Ordnung“. Nicht „der Maintainer sagt es so“. Eine Maschine, die sich nicht umstimmen lässt, hat nach einem Gegenbeispiel gesucht und ist leer zurückgekommen.

Sie mussten uns dafür nicht vertrauen. Sie haben zugesehen, wie es auf Hardware geschah, die Ihnen gehört.

Optional — es absichtlich brechen

Das ist der Teil, der sich lohnt, wenn Sie noch fünf Minuten haben, denn eine Prüfung, die immer nur Ja sagt, ist nicht viel wert.

Öffnen Sie brief_fill_policy_pkg.ads in einem beliebigen Texteditor und ändern Sie die Regel so, dass ein fehlender Speicher eine Antwort trotzdem durchlässt. Führen Sie denselben Befehl erneut aus. Er wird sich weigern — und dabei genau das Theorem nennen, das Sie gerade gebrochen haben.

Diese Weigerung ist das gesamte Sicherheitsmodell. Ghillie installiert nichts, was das nicht besteht, also ist das, was Sie gerade von Hand getan haben, das, was er jedes Mal in Ihrem Namen tut.

Was das nicht beweist

Wir sagen das lieber jetzt, als dass Sie es später herausfinden. Die Beweise decken die Entscheidungsregeln ab — wer was sehen darf, was hinaus darf, was eine Lieferung bestehen muss. Sie machen den Rest der Software nicht magisch, und das behaupten wir auch nicht. Diese Ehrlichkeit ist der Handel, und sie ist der ganze Handel.

Wie es weitergeht

• Der vollständige Rundgang — das Frontend bauen und jede Zeile seiner mitgelieferten Wahrheitstafel prüfen.
• Der Katalog — der Rest des Regals, jedes Stück auf dieselbe Weise neu herleitbar.
• Ghillie — der Assistent, dem diese Regeln dienen.
• Die Riff-Maschine — welche Hardware Sie brauchen, wenn Sie weiter gehen wollen als diese Seite.

Hat es nicht funktioniert, ist das ein Befund, und wir würden gern davon hören. Eine Weigerung, die Sie sich nicht erklären können, ist für uns interessanter als ein Erfolg.