Harmonic 宣称两年内代码全面形式化验证，管理 300 万行代码者逐条反驳
burny_tech · x · 2026-11-05
Harmonic 宣称「两年内所有代码都将被形式化验证」，jiriknesl 引用并给出系统反驳：
- 形式化验证只证明代码符合规约，规约本身可能错——不读 spec 就不知道对错，问题只是被移动了。
- 经济上不成立：证明 1 行代码需要 5-50 行证明；他管理超 300 万行代码，不可能去研读 6000 万行证明和底层假设。
- 合理做法是只对核心（关乎安全、关键业务的几千行代码）做形式化验证，而非全量。
这是 AI 编码可靠性讨论中有分量的反方观点，直指「形式化验证是下一个银弹」的流行叙事。
「漫话AGI」频道最新
- 「Agent 最大化」的隐性代价：让 AI 包办杂事会让你失去品味与创造力 — bendee983 · 2026-11-06
- NYU上海AI与文化中心招博士后，Bogna Konior 指导 — sebkrier · 2026-11-06
- 数学出版或走向人文模式:进展单位是「定论之书」 — prof_g · 2026-11-05
- AI 研究员喊话同行：训练模型本该是最好玩的工作 — code_star · 2026-11-05
- OpenAI 总裁 Brockman：12-18 个月内 AI 将在生物医药取得重大突破 — basedjensen · 2026-11-05
- Ethan Mollick：企业里两股「搞 AI 转型」的力量在暗中角力 — emollick · 2026-11-05