Jane Street智能编码改变看法组建团队让形式化方法成通用工具在过去 25 年里Jane Street 作为一个组织对形式化方法不感兴趣但现在态度转变正在组建一个团队专注于形式化方法。此前Jane Street 虽坚信工具能帮助编写更好、更可靠的代码且从类型系统这种轻量级形式化方法中受益但除特殊情况特别是硬件合成外觉得形式化方法成本效益不高。以 [seL4](https://sel4.systems/) 为例验证 8700 行 C 代码花费了 25 人年的工作量每行代码大约需要 23 行证明验证一行代码需要半天时间。不过智能编码的出现改变了 Jane Street 的看法。一方面它极大地改变了使用形式化方法的成本。虽然智能体本身不能构建任意复杂的证明但模型能让更多人有效地使用这些工具值得重新考虑以往的成本效益计算。另一方面其好处也更大了。一是验证瓶颈比以往任何时候都更加重要。模型生成的代码与实际想要发布的代码存在很大差距存在代码复杂、充满错误和边缘情况、不遵循代码库基本不变量等问题人们需要花费大量时间验证而形式化方法可减轻部分验证负担使代码审查更高效。二是智能体依赖反馈形式化方法是强大的反馈形式可提高智能体解决难题的能力。Jane Street 看到了在使用智能体编程时类型的价值它既有助于缓解验证瓶颈又能为智能体提供更好的反馈。而且Jane Street 有两个优势对所使用语言的深入掌控以及一群对此有准备的程序员。在语言掌控方面Jane Street 能对语言进行调整使其更适合基于证明的技术有很多潜在方向如将属性的模块化规范集成到类型系统中、添加围绕所有权和可变性的类型级约束、直接将证明技术构建到语言中。在程序员方面Jane Street 的程序员比大多数严肃的编程社区更有准备。这里的用户常抱怨新的、奇特的类型系统功能没有尽快推出有很多具备相关背景的人能利用这些技术大家对把事情做好、构建高质量软件有浓厚兴趣。这让 Jane Street 有自由尝试多种方法既能在短期内进行有立竿见影效果的改进也有雄心勃勃的长期愿景。当然Jane Street 也不会忽视外部工作对围绕 [Lean](https://lean-lang.org/)、[Dafny](https://dafny.org/)、[Rocq](https://rocq-prover.org/)、[Agda](https://hackage.haskell.org/package/Agda)、[Iris](https://iris-project.org/) 等工具开展工作的编程语言社区感到兴奋和受到启发也乐意寻找将 OxCaml 与这些工具集成的方法。如果你对此感兴趣不妨考虑申请Jane Street 正在 [伦敦](https://www.janestreet.com/join-jane-street/position/8588405002/) 和 [纽约](https://www.janestreet.com/join-jane-street/position/8585303002/) 招聘人才目前正处于面试阶段正在组建团队。脚注1. 经验表明模型在进行复杂证明时仍需人类帮助和指导。人类程序员可能有对系统工作原理的想法和大致证明思路但大多不知如何将其以符合特定证明系统的方式编码模型可自动完成大部分繁琐工作并在编写证明的技术细节方面提供专业知识。2. 也许不是所有情况像 Obj.magic 这样的逃逸舱可绕过类型级别的约束但可在大部分代码中跟踪并禁止此类异常情况从而获得接近通用保证的效果实际上形式化方法可明确说明使用这些逃逸舱的安全性。Yaron Minsky 于 2002 年加入 Jane Street并声称自己说服公司开始使用 OCaml 是一项“可疑的荣誉”。