我已经告诉人们，在过去的25年里，Jane Street作为一个组织对形式化方法并不感兴趣。现在我不再这样说。并不是说我认为我们多年来的看法是错误的。明确来说，我们坚信工具对帮助我们编写更好更可靠的代码的力量。类型系统是一种轻量级的形式化方法，我们从中获得了巨大的好处。因此，你可能会期望我们对更全面的形式化方法持有坚定的信念。但除了某些特殊情况（尤其是硬件合成），我们一直觉得形式化方法对我们来说不值得那些成本。而那些成本真的非常高！seL4就是一个很好的例子。它是一个形式化验证的微内核，是一个深远的成就。但是，做这个确实非常昂贵！验证8700行C代码花费了25人年的努力，而且每一行代码大约需要23行证明和半个人工作日来验证。我们的希望是让形式化方法成为构建软件时像复杂类型系统一样普遍有用的工具。这种方法在面临高风险且规格相对清晰的安全关键微内核中可能是值得的。但这对大多数软件来说并没有意义，包括我们最关键的软件。因此，随着智能编程的出现，我们的看法发生了变化，我们从怀疑变得对可能性感到兴奋。因此，我们现在正在组建一个团队，专注于形式化方法。我们的希望是让形式化方法成为构建软件时像复杂类型系统一样普遍有用的工具。为什么会有这样的想法转变？智能编程在几个方面动摇了形式化方法的苹果车。一方面，它显著改变了使用形式化方法的成本。并不是说代理们可以自己构建任意具有挑战性的证明。但模型是极其有用的，扩大了可以有效使用这些工具的人群。由于形式化方法比以往更容易使用，所以重新考虑旧的成本/收益计算是值得的。但事情不仅在成本方面发生了变化。好处似乎现在也更大了。对此有两个原因：验证瓶颈比以往更重要。模型在写出有用代码方面越来越出色。但是，模型生成的代码与真正想要发布的代码之间有着很大的差距。在某种程度上，这也与模型的训练方式有关。它们在达到你设定的目标方面表现出乎意料的好，但在维护甚至提高代码库的质量时却做得不是很好。智能代码正在变得更好，但仍然倾向于产生一些混乱：过于复杂、充满奇怪的bug和边界情况，往往不遵循代码库的基本不变性。因此，人们需要花费大量时间验证代理生成的代码是否符合标准。形式化方法可以减轻一些验证负担，并使审查过程变得更加高效。此外，代理在反馈中茁壮成长。这不仅在使用强化学习训练代理时如此，在使用代理编程时也是如此。形式化方法是一种强大的反馈形式，可以增强代理解决难题的能力。我们对于全面形式化方法感到兴奋的很大原因是，我们看到在与代理编程时类型是多么珍贵。并不是说形式化方法是获得反馈的唯一途径。测试也非常有价值，并且通过依靠基于属性的测试和模糊测试，可以让测试变得更好。天知道我们花了多少时间建立测试基础设施。但测试还不够！测试在覆盖程序可能探索的状态空间方面存在固有的局限性。我们在OxCaml编程中看到的一个现象是，代理从普遍保证中受益匪浅，这正是你从类型系统中获得的∀。如果你的类型系统有办法防止数据竞争，你就可以消除所有2个数据竞争。如果你设置你的类型使得跨站脚本漏洞成为不可能，那么你就真的可以完全消除这些漏洞，单靠测试是无法做到的。实际上，我们对于全面形式化方法的兴奋很大程度上是因为，我们看到在与代理编程时类型的价值，无论是减轻验证瓶颈还是为代理提供更好的反馈，这让我们兴奋于利用更强大的证明技术可以带来的更多提升。我们有两个优势：对所使用语言的深刻控制，以及准备好迎接挑战的程序员社区。为什么在这里进行？这个问题引发了一个疑问：为什么Jane Street在处理这个问题时拥有良好的位置？