你的第一份证明

十分钟 · 三个步骤 · 没有什么需要你单凭信任接受

这是入门路线。你不需要是程序员，不需要账号，也不需要告诉我们你的存在。走到最后， 核验一条来自库中真实规则背后的数学的，将是你自己的电脑——不是我们的电脑，也不是我们的 一面之词。

如果你已经熟悉证明器的使用，完整流程会走得 更远：构建前端，并核对其真值表的每一行。这个页面止步于证明本身——这是最要紧的部分， 也是不需要安装任何东西的部分。

你即将核验的是什么

这条规则叫做 brief-fill policy。它决定一个助理何时可以代替主人 回答，而不是去问主人本人。关于它，有四项主张，而这四项都即将在你的机器上接受检验：

• 它从不在没有规则许可的情况下代填一个答案；
• 如果规则存储缺失，什么都不会被放行；
• 它从不凭空发明任何东西；
• 它从不问你一件规则已经回答过的事。

这些不是博客文章里的承诺。它们是定理，而一个证明器即将试图打破它们。

第一步 — 获取证明器

它是免费的，也不是我们的 — 它来自 Ada 社区，而不是来自我们。这正是重点： 核验我们工作的东西，不应该是我们亲手交给你的东西。

第二步 — 获取规则

第一次运行时你可以忽略这个校验和 — 第 3 步的证明并不依赖于它。它是留给你在 想要确认收到的文件就是我们发布的那个文件时使用的，也是目录 所指定的同一个文件。

第三步 — 让你的电脑来核验它

在解包后的文件夹中打开一个终端，运行两行命令：

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

等待。完成后，留意这两个词：

0 unproved

就是这样。这就是整个练习。不需要再安装任何别的东西，而且这一步 在一台什么都没有的普通机器上就能进行 — 你下载的证明器已经带上了这份证明所需的 一切。

刚刚发生了什么

你的电脑拿走了上面那四项主张，试图找出其中任何一项失效的情形，结果找不到 — 因为根本不存在这样的情形。不是“我们测试过，看起来没问题”。不是“维护者这么说”。一台 无法被说服的机器去寻找反例，结果空手而归。

你没有靠信任我们来知道这一点。你是在自己拥有的硬件上，亲眼看着它发生的。

可选 — 故意打破它

如果你还有五分钟，这一部分值得一做，因为一个只会说“是”的核验，价值不大。

用任意文本编辑器打开 brief_fill_policy_pkg.ads，修改这条规则，让一 个缺失的存储也能照样放行一个回答。再次运行同一条命令。它会拒绝 — 并且会指出你 刚刚打破的那条确切定理。

这个拒绝就是整个安全模型。凡是不能通过这一关的东西，Ghillie 都不会安装，所以你 刚刚手动做的这件事，正是他每一次代替你所做的事。

这没有证明什么

我们宁愿现在就把这个说清楚，也不愿让你日后自己发现。这些证明覆盖的是 决策规则 — 谁可以看到什么，什么可以离开，一次送达必须满足什么条件。 它们不会让软件的其余部分变得神奇，我们也从不这样声称。这份诚实就是这笔交易，也是这笔 交易的全部。

接下来去哪里

• 完整流程 — 构建前端，并核对其附带 真值表的每一行。
• 目录 — 架上剩下的一切，每一件都能以同样的方式 重新推导。
• Ghillie — 这些规则所服务的助理。
• 礁的机器 — 如果你想走得比这个页面更远， 需要什么样的硬件。

如果它没有成功，那也是一项发现，我们很想听到。一个你无法解释的拒绝，对我们来说 比一次成功更有意思。