形式化方法与编程的未来

形式化方法与 GenAI 的作用

• 多条评论认为，GenAI 更可能加速形式化方法，而不是相反：AI 可以生成繁琐的证明、规格和样板代码。
• 一种想法是：人类专注于高层规格；LLM 生成杂乱的代码和/或证明，再由机械检查器确保正确性。
• 也有人指出，目前 LLM 生成的证明和验证工件仍然昂贵、脆弱，而且依然需要形式化方法专家来指导。

规格的成本、复杂性与局限

• 多位发帖者表示，针对非平凡系统的完整形式化规格通常比实现本身更大、更复杂，而且可能比代码更晦涩。
• 形式化方法只能保证规格与实现之间的一致性；它们并不能保证规格本身反映现实或不断变化的商业/市场条件。
• 有人担心，严格的系统会促使人们“绕开”它们（类比 Rust 的借用检查器），或者过于紧密的模型只是把错误世界观进一步精炼化。

形式化方法适用的地方（以及不适用的地方）

• 普遍共识是，语义清晰的地方最适合形式化方法：内核、协议、解析器、编译器、密码学、并发原语、硬件、安全关键交易。
• 许多人认为它们是一种“奢侈品”，主要只在高风险或高吞吐量领域才值得；对于初创公司和探索性产品，快速的“进攻式编程”可能更合适。
• 也有人指出，即使是 UI 和许多应用层，也常常可以建模为状态机并从规格中受益，尽管顶层 UX 目标仍然模糊。

形式化方法 vs 测试和基于属性的测试

• 一个关键区别是：测试和基于属性的测试是在抽样行为；形式化方法则试图证明对所有输入和所有执行都成立的性质。
• 不过，编写精确的性质有时会像把函数再实现一遍，而且细微的规格 bug（例如 Unicode 空白定义、整数溢出）仍然会存在。

工具、语言与工作流

• 讨论涉及 Lean、Coq、TLA+、Dafny、SPARK/Ada、Rust 的验证工作，以及主流语言中把类型视为证明的做法。
• 多人强调，应将规格和证明直接集成到编程语言语法中，以避免“阻抗不匹配”。
• 一些人对新兴的“规格驱动开发”和更强的类型系统持乐观态度，认为它们是一个实用的中间地带；另一些人则怀疑形式化方法是否会真正主导日常编程。