文章强调在软件开发中应该优先进行测试而不仅仅是形式验证，指出虽然形式验证有其价值，但测试更能有效发现实际问题。作者认为AI正在推动形式验证的发展，但测试仍然是更实用的方法。

标题：测试优先，而非（仅）验证

作者：Alperen Keles

随着AI技术的崛起，形式化验证正逐渐成为主流。AI辅助的机械证明公司获得巨额融资，越来越多人尝试使用证明助手（尤其是Lean），AI模型在数学竞赛和开放性问题中取得突破性成果。从Terry Tao到Martin Kleppman，全球顶尖研究者都对AI辅助证明充满期待。

形式化验证的优势

1. 规范缺失问题：大多数软件缺乏形式化规范，而AI辅助编程天然适合规范驱动开发，推动编程从"实现能力"向"规范能力"转变。
2. 证明工程挑战：编写系统定理证明非常困难，涉及领域特定知识。但LLM显著提升了证明编写能力，有望实现"描述-形式化-证明-实现"的自动化流程。
3. 成功案例：如CompCert C编译器通过验证，在测试中发现GCC和Clang大量错误，而自身验证部分零错误，展示了形式化验证的价值。

形式化验证的局限

1. 自动形式化基础薄弱：将自然语言描述转化为形式化规范的过程不可验证，成为信任计算基(TCB)中的薄弱环节。
2. 证明助手效率低下：为便于验证使用的数据类型（如Peano数）导致性能问题，提取到高效语言时又引入新的信任假设。
3. 模型构建困难：许多领域（如运行时性能）缺乏合适的理论模型，而测试可以直接利用实际硬件获得真实数据。
4. 反馈机制不足：无法证明不代表定理错误，需要QuickChick等测试工具提供反例验证。

测试与验证的协同

验证引导开发(VGD)模式通过构建两个版本系统： - 简单可验证的参考实现 - 高效的生产实现 通过随机测试确保两者行为一致，兼顾正确性与性能。

结语

作者强调： - 认可形式化验证的价值 - 但反对过度承诺 - 随机测试与形式化验证同等重要 未来软件工程需要验证与测试的结合，才能实现"正确性成为常态"的理想。

（注：原文中的社交媒体链接、图片描述等非核心内容已省略，保留了主要技术论点和案例）

这篇评论围绕AI辅助编程与形式化验证展开讨论，主要呈现以下观点：

1. 对形式化验证的质疑

• 认为形式化验证尚未成为主流，实施难度大："No it isn't...I'm sure the people selling it wish it was"(badgersnake)
• 指出当前更现实的验证方式："Most people can't even get agents to robustly E2E QA code"(CuriouslyC)

2. 支持验证重要性的观点

• 强调验证概念的价值："learning the concept of invariants...makes reasoning about code easier"(zipy124)
• 建议从基础验证开始："start with something 'dumber' like Rust or any typed program"(anon-3988)

3. 关于AI辅助验证的讨论

• 认可AI改变验证瓶颈："pushes the bottleneck to verification"(andrewmutz)
• 但指出局限性："adversarial agents...still get tripped up"(tgtweak)
• 担忧数据问题："AI need tons of training material...large scale synthetic generation"(ecocentrik)

4. 实用主义观点

• 推荐折中方案："TDD gets you a lot of them as well"(andrewmutz)
• 强调测试必要性："all software needs testing"(MetaWhirledPeas)
• 指出现实限制："people cant even bother to write code"(throw-12-16)

5. 技术实现讨论

• 区分验证级别："distinguish between a full specification...and a specification of certain properties"(vzaliva)
• 质疑AI验证效率："many possible ways...be terrible in terms of performance"(xp84)