Why Don't People Use Formal Methods?
5 hours ago
- 形式化方法分为形式化规范（编写精确规格）和形式化验证（证明正确性），并进一步细分为代码与设计领域。
- 代码验证困难且成本高昂，历史上依赖手动证明，通过如Z3的SMT求解器取得了进展，但完全验证仍然缓慢（例如，每天约4行）。
- 部分代码验证（例如，证明无崩溃）更为实用，并可嵌入类型系统（例如，Rust用于内存安全）。
- 设计验证比代码验证更容易，常使用模型检查器暴力搜索状态空间，但面临文化阻力且缺乏感知价值。
- 关键障碍包括证明的难度、根据用户需求验证规范的挑战，以及社会对采用非代码工件的抵触。
- 许多高保证技术（例如，Cleanroom）无需完全形式化验证即可实现近乎完美的软件，使其对大多数工业用途而言变得不必要。