我一直对依赖类型语言如 Coq Rocq 和 Lean 有着浓厚的兴趣。它们提供了一种能够编码和强制执行任意细微不变式的类型系统的可能性。在常规语言中，这种东西充其量只是注释，随着团队规模的扩大而迅速消失。然后你会遇到微妙的误解和不太契合的组件。通常情况下，这些组件已经变得足够大，当问题被发现时，重新对齐它们的前景是令人疲惫的。也许，例如依赖类型诱人地说，你可以正式编写这些不变式，并让机器检查它们。 （附：Coq 改名了！我记得在普林斯顿的一次 Coq 会议上，多年前我曾试着建议过，在一个讲英语的世界中，拥有一个叫 Coq 的编程语言是一种障碍。我当时认为听众并不同意。我还开玩笑说，那里的许多演讲听起来像是提利昂·兰尼斯特的演讲，因为有那么多的 Coq 和 Hoare。这是一个既好笑又恰到好处的玩笑，尽管它完全没有效果，因为它出现在那个节目最终季之前以及我们集体掩盖它的记忆之中。）问题一直是，强大的类型系统带来了巨大的证明工作。我可以肯定地说，曾经有整整一天的时间用来证明非常简单的事情。做证明实际上是相当有趣的：它具有挑战性、互动性，并且有明确的目标。但是，天哪，这需要很多时间，尤其是如果你像我一样，不知道自己在做什么。还有一种定期出现的、令人恼火的经历，在数小时的努力结束时，你意识到你试图证明的目标实际上是错误的。这里的经典结果是 seL4 项目的回顾，发现尽管项目足够大，让工程师们积累了相当的经验，但他们花在证明上的时间大约是设计和实现时间的 10 倍。他们最终的证明代码行数比 C 代码多出了 20 倍以上。这种开销使得在依赖类型语言中编程变得极其小众。它也促使人们尝试自动化这一过程。我偶尔熟悉的尝试是 F*，该系统试图让 SMT 求解器自动解除义务。这在简单情况下确实有效，但很容易构造出使 SMT 求解器进入无穷大并运行数小时的示例，让你怀疑它是否会完成。我看到经常使用这些语言的人必须培养出一种第六感，了解什么会让求解器开心，然后围绕这个构建一切。这可以有所帮助，但在某种程度上，它将问题转变为神秘主义：你最终是在为一个复杂而善变的神服务。一个关键的事实是，至少在理论上，一旦语句正确，它的证明内容就不重要：只要它存在即可。这并不完全正确，因为有两个复杂的因素：首先，seL4 组所称的 "证明工程"：需要结构化证明，从而在代码更改后重新对齐的工作量减少。其次，复杂的证明可能会导致甚至类型检查器崩溃并消耗大量内存。我们现在有了 LLMs，它们结合证明无关性，承诺成为一种极具能力的证明自动化形式。随着自动化程度的提高，或许你不需要如此担心证明工程。你仍然需要避免让类型检查器崩溃，但在我有限的测试中，LLMs 能够避免这一点。LLMs 或许突然使得依赖类型系统变得更加实用。我想尝试一下这个，所以在 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，log 规模)——越高越快 （测量在标准参考计算机上进行，即作者当时使用的任何计算机。请注意 y 轴上的对数比例：gzip 和 Zstandard 在它们自己的速度类别中。这是一台 Apple 机器，Apple 的 gzip 优化特别到位；预计在其他地方 gzip 会更慢。）Zstandard （由 Yann Collet 提供，基于 Jarek Duda 的开创性 ANS 研究）有一份 RFC，但内容相当简洁。