来源笔记
Formal Methods and the Future of Programming
摘要
Jane Street 说，代理式编程让形式化方法在软件生产中更实用，也更有价值。文中认为，证明工具可以减轻代码评审负担，给代理更好的反馈，并帮助强制执行测试覆盖不到的代码库不变量。
问题
- 代理生成的代码在发布前通常需要大量人工审查。
- 测试只覆盖状态空间的一部分，因此会漏掉一些漏洞和不变量违规。
- 对大多数软件来说，完整形式化验证的成本一直太高，所以采用范围一直有限。
方法
- 使用代理和模型来降低编写和维护证明的成本。
- 把形式化方法当作编码代理的反馈信号，和测试、基于属性的测试一起使用。
- 扩展编程语言 OxCaml，加入更强的类型级约束、模块化规格和更适合证明的特性。
- 把语言设计和证明工具结合起来，让日常开发里更容易表达和检查保证。
结果
- 摘要里没有报告定量实验结果。
- 最强的说法是战略层面的：代理式编程改变了成本和收益的平衡，Jane Street 因此正在组建一个形式化方法团队。
- 文中把 seL4 作为旧式验证的成本基线：验证 8,700 行 C 代码用了 25 人年，每行代码大约对应 23 行证明，并且每行代码大约需要半个人天来验证。
- 文中说，当类型系统里编码了相应约束时，类型已经可以消除数据竞争、跨站脚本这类整类缺陷。
- 文中认为，形式化方法可以减少代理编写代码的验证工作，并提高代理在困难任务上的表现，但没有给出基准数字。