我们现在有证明自动化

ImperialViolet 我们现在拥有自动化证明（2026 年 7 月 26 日） 我长期以来一直对 Coq Rocq 和 Lean 等依赖类型语言情有独钟。它们提供了一种能够编码和执行任意微妙的不变量的类型系统的可能性。这种东西，在常规语言中，最终（最多）是一条评论，但随着团队规模的扩大，它很快就会消失。然后你就会产生微妙的误解和不完全配合的组件。通常情况下，这些组件已经增长到足够大的尺寸，当发现问题时，对齐它们中的任何一个都是一个令人厌烦的前景。也许，诱人地说依赖类型，您可以正式编写这些不变量并让机器检查它们。 （注：Coq 改名了！我记得很多年前在普林斯顿举行的 Coq 会议上，我试图建议，在英语世界中，拥有一种名为 Coq 的编程语言是一种障碍。我认为当时的观众并不同意。我还开玩笑说，那里的许多演讲听起来像提利昂·兰尼斯特的演讲，有那么多 Coq 和 Hoares。这个笑话很搞笑，很及时，尽管它完全平淡了，就像该剧最后一季之前发生的那样，以及我们对它的集体记忆。）问题始终是，强大的类型系统能力带来了巨大的证明工作。我当然可以证明我花了一整天的时间来证明非常简单的事情。做证明实际上很有趣：它具有挑战性、互动性并且有明确的目标。但是天哪，这是否需要很多时间，特别是如果你像我一样不知道自己在做什么。还有一种周期性的、令人痛苦的经历，在许多小时的努力结束时，你意识到你试图证明的目标实际上是错误的。这里的经典结果是对 seL4 工作的回顾，该结果发现，尽管该项目足够大，足以让工程师积累丰富的经验，但他们在证明上花费的时间大约是设计和实现的时间的 10 倍。他们最终得到的证明代码行数是 C 代码的 20 多倍。这种开销使得依赖类型语言的编程变得非常小众。它还促使人们尝试将其自动化。我所熟悉的尝试是 F*，其中系统尝试让 SMT 求解器自动履行义务。这当然适用于简单的情况，但很容易制作一些导致 SMT 求解器进入太空并运行数小时的东西，让您想知道它是否会完成。我发现经常使用这些语言的人必须培养第六感才能让求解器感到高兴，然后围绕它来设计一切。它可以有所帮助，但在某种程度上它把问题转化为神秘主义：你最终服务的是一个复杂而善变的神。一个关键的事实是，至少在理论上，一旦陈述正确，其证明的内容就无关紧要：只有它的存在才是重要的。这并不完全正确，因为有两个复杂的因素：首先，seL4 小组所谓的“证明工程”：需要构建证明，以便减少代码更改后重新调整它们的工作量。其次，足够复杂的证明甚至可能导致类型检查器崩溃并消耗大量内存。我们现在拥有法学硕士，再加上证明无关性，有望成为一种极其强大的证明自动化形式。有了足够的自动化程度，也许您几乎不需要担心证明工程。你仍然需要避免破坏类型检查器，但在我有限的测试中，法学硕士可以避免这种情况。法学硕士有可能突然使依赖型系统变得更加实用。我想尝试一下，所以用 Lean 构建了一个 Zstandard 解压器，主要是因为我对 Zstandard 也很好奇。 Zstandard 似乎正在赢得取代 gzip 成为规范压缩实用程序的竞争。它是另一种 LZ77 风格的压缩器，但它提供了更好的熵编码和精心的设计，使其能够实现非常令人印象深刻的解压缩速度。它永远不会像 bzip2 那样美丽，但在显着的实际优势面前，Burrows–Wheeler 变换的闪亮优雅并没有多大意义： zstd bzip2 gzip lzma (XZ/LZMA2) 50 100 200 500 1000 2000 zstd bzip2 gzip lzma (XZ/LZMA2) 70 72 74 76 78 80 82 84 86 在 64 MiB Lean/mathlib 源代码上的压缩权衡 节省的空间 (%) — 越往右压缩越多 解压缩吞吐量（MiB/s，对数刻度） — 越高则速度越快（在标准参考计算机上进行的测量，即作者当时使用的任何计算机。并注意 y 轴上的对数刻度：gzip 和 Zstandard 处于其自己的速度等级。这是 Apple 机器和 Apple 的机器gzip 特别优化；预计 gzip 在其他地方会更慢。） Zstandard（由 Yann Collet 构建，建立在开创性的 ANS 基础上）