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 是一项“可疑的荣誉”。
