Ваше перше доведення

десять хвилин · три кроки · нічого, що треба брати на віру

Це шлях для початківців. Вам не потрібно бути програмістом, вам не потрібен обліковий запис, і вам не потрібно повідомляти нам, що ви існуєте. Наприкінці цього шляху ваш власний комп'ютер — не наш, і не наше слово про це — перевірить математику, що стоїть за справжнім правилом із бібліотеки.

Якщо ви вже впевнено орієнтуєтеся в доводчику, повний посібник іде далі: збирає фронт і перевіряє кожен рядок його таблиці істинності. Ця сторінка зупиняється на доведенні — тій частині, яка важлива найбільше і не потребує нічого встановлювати.

Що ви зараз перевірите

Правило називається brief-fill policy. Воно вирішує, коли помічник може відповідати від імені свого власника замість того, щоб питати його. Про нього роблять чотири твердження, і всі чотири зараз буде перевірено на вашій машині:

Це не обіцянки з блог-допису. Це теореми, і доводчик зараз спробує їх спростувати.

Крок 1 — отримайте доводчик

github.com/alire-project/GNAT-FSF-builds/releases/tag/gnatprove-16.1.0-1

Візьміть файл для вашої машини:

Розпакуйте його будь-де. Жодного встановлювача немає, нічого не потрапляє у вашу систему, і ніщо не працює у фоні. Видаліть теку, коли закінчите, — і все буде так, ніби цього не було.

Це безкоштовно, і це не наше — це походить від спільноти Ada, а не від нас. У цьому й суть: те, що перевіряє нашу роботу, не повинно бути тим, що вручили вам ми. Одна чесна обмовка щодо «десяти хвилин»: відлік починається після того, як це завантажиться, а важить це кілька сотень мегабайтів — швидко на хорошій лінії, повільніше на поганій.

Крок 2 — отримайте правило

brief-fill-policy.tar.gz (6 918 байт)

sha256: 14bb06671459784d2d571e7b5e2afc3037894c241517612b026dbe053fb6b180

Розпакуйте його. Усередині — джерельний код, доведення і опис того, що робить правило, простою мовою.

Під час першого запуску ви можете проігнорувати контрольну суму — доведення в кроці 3 від неї не залежить. Вона потрібна, коли ви захочете підтвердити, що отриманий вами файл — це той файл, який опублікували ми, і що це той самий файл, який називає каталог.

Крок 3 — попросіть свій комп'ютер це перевірити

Відкрийте термінал у розпакованій теці і виконайте два рядки:

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

Зачекайте. Коли все завершиться, знайдіть ці два слова:

0 unproved

Це все. Це вся вправа цілком. Більше нічого встановлювати не потрібно, і цей крок працює на звичайній машині, на якій більше нічого немає — доводчик, який ви завантажили, несе все, що потрібно доведенню.

Що щойно відбулося

Ваш комп'ютер узяв чотири твердження вище, спробував знайти випадок, у якому хоч одне з них не виконується, і не зміг — бо такого випадку немає. Не «ми це протестували, і начебто все гаразд». Не «так каже супровідник». Машина, яку не можна умовити, шукала контрприклад і повернулася ні з чим.

Ви не повірили нам на слово, що це так. Ви побачили, як це відбувається, на залізі, яке належить вам.

Додатково — зламайте це навмисно

Це варто зробити, якщо у вас є ще п'ять хвилин, бо перевірка, яка завжди каже «так», коштує небагато.

Відкрийте brief_fill_policy_pkg.ads у будь-якому текстовому редакторі і змініть правило так, щоб відсутнє сховище все одно пропускало відповідь. Запустіть ту саму команду знову. Вона відмовить — і назве саме ту теорему, яку ви щойно зламали.

Ця відмова і є вся модель безпеки цілком. Ghillie не встановлює нічого, що цього не проходить, тож те, що ви щойно зробили вручну, — це те, що він робить від вашого імені щоразу.

Чого це не доводить

Ми краще скажемо це зараз, ніж дозволимо вам виявити це пізніше. Доведення охоплюють правила ухвалення рішень — хто може бачити що, що може піти, що повинна пройти кожна доставка. Вони не роблять чарівним решту програмного забезпечення, і ми не стверджуємо протилежного. Ця чесність і є угода, і це вся угода.

Куди рухатися далі

Якщо не спрацювало — це знахідка, і нам хотілося б про неї почути. Відмова, яку ви не можете пояснити, цікавіша нам, ніж успіх.