形式化方法与编程的未来
过去 25 年来，我一直在告诉别人：作为一家公司，Jane Street 对形式化方法（formal methods）不感兴趣。
现在我不再这么说了。
倒不是说我觉得我们过去错了。清楚地说，我们深信工具可以帮助我们编写更好、更可靠的代码。类型系统本身就是一种轻量级的形式化方法，我们从中获益巨大。所以你可能觉得我们会是更“正经”的形式化方法的坚定信徒。
但除了某些特殊情况（特别是硬件综合），我们一直觉得形式化方法对我们来说不值那个成本。而那些成本真的很高！seL4 就是一个很好的例子。它是一个经过形式化验证的微内核，堪称一项深远的成就。但是，做这件事的成本真的很高！验证 8,700 行 C 代码花了 25 人年，每行代码需要大约 23 行证明和半人天来验证。
那种方法对安全关键的微内核可能是值得的——因为风险高、规格清晰。但对大多数软件来说根本不可行，而且对我们来说，连我们最关键的那些软件都不值得这么干。
但智能体编程（agentic coding）的出现改变了我们的看法，我们从怀疑变成了兴奋。结果是，我们现在正在组建一个专注于形式化方法的团队。我们的希望是让形式化方法成为构建软件时普遍好用的工具，就像今天成熟的类型系统对我们是多么好用一样。
为什么改变想法？
智能体编程从几个方面颠覆了形式化方法的天平。
一方面，它极大地改变了使用形式化方法的成本。不是说智能体能自己构建任意复杂的证明。1但模型非常有帮助，它拓宽了能高效使用这些工具的人群范围。既然形式化方法比以往任何时候都更容易使用，那就有必要重新考虑旧的成本效益计算了。
但变化的不仅仅是成本一侧。收益现在也看起来更大了。这主要有两个原因：
验证瓶颈比以往任何时候都更重要。模型越来越擅长编写有用的代码。但模型生成的代码和你真正愿意发布的代码之间存在着巨大的差距。某种程度上，这是模型训练方式造成的。它们在完成你设定的目标方面出奇地好，但在维护甚至改善代码库质量方面却做得不够好。智能体代码在进步，但仍然倾向于“敷衍”：过于复杂、充满奇怪的 bug 和边界情况，通常不遵循它所属代码库的关键不变量。
结果就是，人们需要花大量时间来验证智能体生成的代码是否达标。而形式化方法可能是减轻这种验证负担的一种方式，能让审查过程更高效。
另外，智能体依赖反馈。无论你在用强化学习训练智能体时，还是用智能体来编程时，这都是事实。而形式化方法是另一种强大的反馈形式，可以提升智能体解决难题的能力。
不是说形式化方法是获取反馈的唯一途径。测试也非常有价值，而且可以通过引入基于属性的测试和模糊测试变得更好。天知道我们在测试基础设施上投入了多少精力。
但测试还不够！测试在覆盖程序可能探索的状态空间方面存在天然限制。我们在自己的 OxCaml 编程实践中看到的一件事是，智能体从全局保证（universal guarantees）中获益巨大——也就是类型系统中蕴含的那种“对所有情况都成立”的保证。如果你的类型系统能够防止数据竞争，你就能消除所有2数据竞争。如果你把类型设计得让跨站脚本攻击不可能发生，那你就真的能彻底消除这类问题，而纯靠测试很难做到这一点。
事实上，我们对全面的形式化方法感到兴奋的很大一部分原因，正是我们看到在与智能体一起编程时类型系统是多么有价值——既缓解了验证瓶颈，又为智能体提供了更好的反馈。这让我们迫不及待地想看看，利用更强大的证明技术还能带来多大的提升。
为什么在 Jane Street 做这件事？
这引出一个问题：为什么 Jane Street 在解决这个问题上有优势？全世界都在思考智能体对编程未来的意义，也有无数创业公司在寻找将形式化方法和智能体结合的方式。为什么我们要在内部做这件事？为什么外部的形式化方法专家会愿意加入我们的努力？
一方面，我们对我们使用的语言有深层的控制力，这让我们能够调整这门语言，让它成为面向证明的技术的更好家园。这里有大量的潜在方向：从将模块化的属性规范集成到类型系统中，到在类型层面增加关于所有权和可变性的约束以使某些证明更容易，再到将证明技术直接构建到语言中。
我们还有一群做好了准备的程序员社区，至少比我遇到过的任何严肃编程社区都更有准备。对大多数从事编程语言工作的人来说，容易的部分是想出新的、更好的点子来改进编程。难的部分是说服有人真正把这些点子用在实际工作中。
在 Jane Street，情况完全不同！我们的用户经常因为我们承诺给他们的新奇、古怪的类型系统特性来得不够快而生气。我们有很多具备正确背景的人来利用这些技术，也有着深厚的兴趣去做正确的事情、构建高质量的软件。
我们认为这样的用户群会给我们尝试多种方法的自由——有些近期的改进我们认为能很快产生效果，也有一些更雄心勃勃的长期愿景需要几年时间来实现。拥有一个投入且兴奋的用户群使得这两种方法都成为可能，让我们能在构建长期愿景的同时，从短期实践中学习。
这不是说我们会忽视外部世界的工作。我们对其他编程语言社区的工作感到兴奋和启发，这些社区围绕 Lean、Dafny、Rocq、Agda、Iris 等工具展开（太多无法一一列举）。我们也很愿意寻找将 OxCaml 与其中一些工具整合的方法，以利用已有优秀基础设施。但我们也相信，只有同时从语言层面和证明技术层面入手，才能实现某些独特的优势。
加入我们！
如果你觉得这听起来很有意思，不妨考虑申请！我们在伦敦和纽约都在招人。我们还处于组建团队和面试的早期阶段，前面有大量的工作等着我们，欢迎你加入其中。
脚注
-
我们的经验是，模型在导航复杂证明时仍然需要人类的帮助和指导。人类程序员可能知道一个系统为什么能工作，以及从高层如何着手证明它。但大多数程序员不知道如何将这些证明想法编码成某个证明系统能接受的形式。模型可以自动化大量繁琐的工作，并在写出证明的技术细节方面提供现成的专业知识。↩
-
好吧，可能不是“所有”。有一些逃生舱，比如
Obj.magic，可以绕过类型层面的约束。但你可以追踪并禁止那些大多数代码中异常，到那时你确实能得到非常接近全局保证的效果。而且，形式化方法也可以让你明确说明为什么使用这些逃生舱实际上是安全的。↩
原文链接：Jane Street Blog
