为什么人们不用形式化方法？（2019）
用于证明软件正确性的形式化方法在日常开发中仍然很少见，主要因为它们难学、应用成本高，而且常被认为对 CRUD 应用或社交平台等低风险场景没有必要。评论者指出，严格技术主要被采用在失败代价极高的领域（例如硬件设计、数据库、金融、关键系统），而类型系统、lint 工具和部分验证等轻量形式才是最实用的折中方案。也有人认为 AI 工具和更好的工具链可以降低使用门槛，但同时强调，形式化证明仍然会把问题转移到编写准确规格上，而规格本身可能和代码一样复杂且容易出错。
感知价值与业务背景
- 许多人认为，形式化方法很少能证明其成本合理：大多数软件都是低风险的 CRUD、原型，或不断变化的业务应用，在这些场景下快速迭代比严格证明更重要。
- 人们认为更高的投资回报率出现在基础设施和安全关键领域（数据库、文件系统、硬件、金融、密码学、航空电子、医疗、DeFi），但即便如此，采用也并不均衡。
- 有些人把这种未被广泛使用看作是风险管理不佳和“快速行动”文化的症状；另一些人则更简单地将其视为理性的 ROI 优化。
难度、教育与文化
- 一个反复出现的主题是：形式化方法很难学、在智力上要求很高，而且解释得不好；许多工程师对此感到畏惧或没有兴趣。
- 还有对该用哪种方法的困惑；人们想要的是“一种适用于一切的次优方案”，而不是一整套技术的动物园。
- 形式化方法的倡导者报告说，他们在公司内部常常遭遇阻力，并且经常会把这些方法“偷偷”引入工作流。
规格与代码及其局限
- 多条评论强调，规格说明可能和代码一样复杂；漏洞只是从实现层转移到了规格层。
- 排序被用来说明一个“完整”规格有多微妙（必须描述顺序、长度、排列、重复项、并列情况）。
- 形式化方法被视为测试的补充，而不是替代；两者最终都依赖于人类对需求的理解。
类型、部分验证与务实技术
- 许多人指出，类型系统、lint 工具及相关分析已经广泛使用，可视为“轻量级形式化方法”。
- 大家也在争论“类型检查”在哪里结束、“形式化验证”在哪里开始；有些人坚持至少要有细化类型式的约束才算。
- 部分验证（例如证明关键属性或小型纯组件）被认为是实用的，尤其适用于库、编解码器和并发算法。
工具、示例与案例研究
- 工具链被认为是碎片化且难以上手的；人们希望有适合初学者的、开源的、首选方案，以及非玩具级的示例（例如文本编辑器、待办事项应用）。
- 据说硬件和一些大型软件公司会使用更重型的形式化工具；有一位从业者在用 Rust 重写数据库引擎时，使用模型检测证明了 1000 多个函数的等价性，并发现了微妙的上游漏洞。
- 还有人称一些大型云服务提供商会使用形式化模型进行设计和遥测验证，但具体细节和使用范围存在争议。
LLM 与未来方向
- 一些人推测，LLM 可能会通过以下方式改变局面：
- 大规模生成候选证明或规格，而验证它们比生成它们更便宜。
- 让非专家也能更容易地试验 TLA+、Lean 以及其他工具。
- 也有人警告说，把形式上精确的规格输入黑盒模型，会引入另一层同样必须被信任或检查的环节。