文章核心内容：作者过去25年认为形式化方法不值得投入，但现在改变了看法。虽然形式化方法成本高昂（如验证8700行代码耗时25人年），但作者希望未来能让形式化方法像类型系统一样成为普遍实用的软件开发工具，特别是在安全关键领域。

标题：形式化方法与编程的未来

核心观点转变

过去25年间，Jane Street对形式化方法始终持保留态度。尽管我们认可类型系统等轻量级形式化工具的价值，但传统形式化方法（如seL4微内核验证）的高昂成本（验证8,700行C代码需25人年）使其难以普及。然而，智能体编程（Agentic Coding）的兴起彻底改变了这一局面，促使我们组建专门团队探索形式化方法的应用，目标是使其像现代类型系统一样成为软件开发的基础工具。

转变动因

1. 成本降低：
   智能体虽无法独立完成复杂证明，但能显著降低形式化方法的使用门槛，扩大适用人群。
2. 需求提升：
   • 验证瓶颈：智能体生成的代码常存在冗余、边界错误和违反代码库不变量的问题，人工验证耗时。形式化方法可高效保证代码质量。
   • 反馈强化：形式化验证为智能体提供结构化反馈，提升其解决复杂问题的能力（尤其在强化学习场景中）。

形式化方法的独特优势

• 超越测试的覆盖性：类型系统能全局消除特定问题（如数据竞争、跨站脚本漏洞），而测试仅能覆盖有限状态空间。
• 与智能体的协同效应：形式化方法既能缓解验证压力，又能通过严格约束优化智能体的代码生成。

Jane Street的独特优势

1. 语言控制力：可深度定制OxCaml等语言，集成模块化规范、所有权约束等特性，直接支持形式化验证。
2. 开发者生态：内部团队对创新工具接受度高，甚至主动要求增强类型系统功能，为实验提供理想环境。
3. 内外协作：将借鉴Lean、Dafny等外部工具，同时探索语言与验证技术深度结合的独家方案。

行动号召

Jane Street正在伦敦和纽约招募形式化方法专家，共同构建下一代编程范式。

背景备注：
- seL4案例：验证成本约23行证明/代码行 + 0.5人日/代码行。
- 智能体编程的局限：需人类指导高阶证明思路，但能自动化底层证明细节。
- 类型系统例外：如Obj.magic可绕过约束，但形式化方法能显式验证其安全性。

（作者Yaron Minsky自2002年推动Jane Street采用OCaml，现主导形式化方法转型。）

精简说明：
- 保留成本效益分析、智能体编程的双向影响（成本↓/需求↑）、类型系统对比测试的核心逻辑链。
- 删减部分工具链细节（如具体测试方法）、次要案例（如OxCaml数据竞争），聚焦形式化方法与智能体的协同主线。
- 合并重复论述（如反馈机制在验证与训练中的作用）。

以下是评论内容的总结，平衡呈现不同观点并保留关键引用：

支持形式化方法的观点

1. 可复用验证系统的价值

   • 认为应投资可复用的验证系统（如类型系统），通过大规模应用摊薄成本："investing that huge amount of labor... will now pay off" (eddiepete)
   • Lean4等工具结合AI可提升效率："AI + formal systems is a dramatically bigger leap" (reinitctxoffset)

2. 特定场景的高适用性

   • 适用于算法确定性强的领域（如金融）："Jane Street maintains large code bodies where the mapping is 1:1" (spenrose)
   • 已验证案例："We've done millions of lines... property tested and multiply fuzzed" (reinitctxoffset)

质疑形式化方法的观点

1. 验证成本与局限性

   • 验证代码本身可能存在问题："isn’t the verification code going to be sloppy as well?" (eddiepete)
   • 形式验证非万能："seL4 despite being formally verified contained gnarly bugs" (xvilka)

2. 理论与实践的鸿沟

   • 过度形式化可能脱离实际需求："humans tend to find ways around it... writing code only for specific formalized answers" (jdw64)
   • 领域适配性问题："how closely do the postulates fit the domain?" (spenrose)

中立/技术探讨观点

1. 工具成熟度问题

   • 现有工具体验不佳："custom linters are still pretty bad to write" (awinter-py)
   • 历史经验提示自动化重要性："Later systems seemed to have less automation" (Animats)

2. 方法论演进

   • 形式化方法需与语言深度集成："verification statements integrated into the programming language" (Animats)
   • 新范式可能兴起："Spec-Driven Development as the Rational Unified Process revenge" (pjmlp)

关键争议点：形式化方法是否真能解决AI时代代码量激增带来的质量问题，抑或只是将瓶颈转移至验证环节。支持者强调可复用性和特定领域价值，反对者则质疑其普适性和实际成本。