形式化方法与编程的未来

# 形式化方法与编程的未来 来源：https://blog.janestreet.com/formal-methods-at-jane-street-index/ 过去25年里，我一直告诉别人，简街作为一家组织对形式化方法没什么兴趣。 我现在不再这么说了。 倒不是说我认为这些年来我们错了。明确地说，我们坚信工具能帮助我们写出更好、更可靠的代码。类型系统就是一种轻量级的形式化方法，我们从中受益匪浅。所以你可能以为我们会更热衷于更全面的形式化方法。 但除了某些特殊情况（尤其是硬件综合），我们的感觉是形式化方法对我们来说得不偿失。而代价确实很高：seL4 就是一个很好的例子。它是一个经过形式化验证的微内核，是了不起的成就。但是，天哪，做起来可真贵！(https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf) 验证 8700 行 C 代码花了 25 人年，每行代码大约需要 23 行证明和半人天的验证。 我们的希望是让形式化方法成为一种像今天成熟的类型系统那样普遍有用的软件构建工具。 这种方法对于安全关键的微内核可能是值得的，因为风险高、规格明确。但对于大多数软件来说并不合理，而且对我们来说，即使是关键软件，感觉也不太适用。 但智能体编程的出现改变了我们的看法，我们从怀疑变成了对这个可能性的激动。因此，**我们现在正在组建一个专注于形式化方法的团队**。我们的希望是让形式化方法成为一种像今天成熟的类型系统那样普遍有用的软件构建工具。 ## 为什么转变了想法？ 智能体编程在几个方面颠覆了形式化方法的格局。 首先，它极大地改变了使用形式化方法的成本。并不是说智能体能独立构建任意复杂的证明¹。但模型非常有帮助，并扩大了能有效使用这些工具的人群范围。随着形式化方法比以往任何时候都更容易使用，重新考虑旧的成本/收益计算是值得的。 但成本方面并非唯一的变化。现在收益似乎也更大了。这主要有两个原因： **验证瓶颈比以往任何时候都更重要**。模型在编写有用代码方面越来越好。但模型生成的代码与实际可以发布的代码之间存在巨大差距。某种程度上，这是模型训练方式造成的。它们在实现你设定的目标方面出奇地好，但在维护甚至提高代码库质量方面做得并不好。智能体代码在进步，但仍然倾向于“草率”：过于复杂，充满奇怪的错误和边界情况，往往不遵循代码库的基本不变量。 因此，人们需要花大量时间验证智能体生成的代码是否达标。而形式化方法可以减轻部分验证负担，使审查过程高效得多。 此外，**智能体依赖反馈**。这在用强化学习训练智能体时，以及用智能体编程时都是如此。而形式化方法是另一种强大的反馈形式，可以提高智能体解决难题的能力。 我们之所以对全面的形式化方法感到兴奋，很大程度上在于看到了用智能体编程时类型的价值。 当然，形式化方法不是获得反馈的唯一途径。测试也非常有价值，并且可以通过利用基于属性的测试和模糊测试变得更好。而且天知道我们花了多少时间构建测试基础设施。 但测试还不够！测试在覆盖程序可能探索的状态空间方面存在固有局限。我们在自己的 OxCaml 编程中看到的一件事是，智能体从通用保证中获益巨大，即从类型系统中获得的 ∀。如果你的类型系统能防止数据竞争，它就能消除所有数据竞争。如果你设置类型使跨站脚本攻击不可能，那么你就能真正完全消除它们，而仅仅通过测试很难做到。 事实上，我们之所以对全面的形式化方法感到兴奋，很大程度上在于看到了用智能体编程时类型的价值——既能缓解验证瓶颈，又能为智能体提供更好的反馈。这让我们好奇，通过利用更强大的证明技术，还能获得多大的提升。 我们有两个优势：对我们使用的语言有深入控制，以及一群准备好了的编程人员。 ## 为什么在这里做？ 这引发了一个问题：为什么简街有条件解决这个问题？全世界都在思考智能体对编程未来的意义，有无数初创公司在寻找混合形式化方法和智能体的方法。为什么我们要内部做这件事？为什么外部世界的形式化方法专家会乐于加入我们的努力？ 首先，**我们对我们使用的语言有深入控制**，这使我们能够调整该语言，使其更适合面向证明的技术。这里有多种可能的方向：从将属性的模块化规范集成到类型系统中，到添加关于所有权和可变性的类型级别约束以简化某些证明，再到将证明技术直接内置到语言中。 我们还**拥有一个准备好了的编程人员社区**，或者至少比我见过的任何严肃编程社区都更准备好。对于大多数从事编程语言工作的人来说，容易的部分是想出新的更好的想法来改进编程。难的部分是说服别人在实际工作中使用这些想法。 在简街，情况不同！我们经常有用户因为新奇的类型系统特性来得不够快而对我们生气。我们有很多具备正确背景的人来利用这些技术，并且对把事情做好、构建高质量软件有浓厚的兴趣。 我们认为这个用户群会让我们自由地尝试多种方法；有些近期的改进我们认为可以产生立竿见影的效果，还有一些雄心勃勃、更长期的愿景——几年内我们可能达到的目标。拥有一个积极参与和兴奋的用户群使得这两种方法都成为可能，并让我们在建设长期目标的同时从前者中学习。 这并不意味着我们会忽略外部世界的工作。我们对其他各种编程语言社区的工作感到兴奋和启发，这些社区围绕 Lean、Dafny、Rocq、Agda、Iris 等工具建立，还有太多无法一一提及。我们也很期待寻找将 OxCaml 与其中一些工具集成的方式，以利用已有的优秀基础设施。但我们认为，只有同时处理语言和证明技术，才能实现某些独特的优势。 ## 加入我们吧！ 如果你对此感兴趣，请考虑申请！我们在伦敦和纽约都在招人。我们正处于为这些职位面试和组建团队的早期阶段，前面还有大量工作要做，我们很乐意你成为其中一部分。 Yaron Minsky 于 2002 年加入简街，并声称是他说服公司开始使用 OCaml 的——这个荣誉值得怀疑。