Bend 2 and the Vibe-Coding Trap
2 hours ago
- Bend 2 要求开发者为了简单属性编写冗长的规则（58行）和证明（442行），同时依赖AI生成实现。
- 当开发者在未充分调研的情况下构建大型解决方案，从而错失已有的更优方法时，便陷入了“氛围编码陷阱”。
- Bend 的作者似乎对形式验证领域毫无了解，因为该术语并未出现在 Bend 的文档或代码库中。
- SPARK 是一种已有的形式验证语言，可以使用 GNATprove 等工具，用更少的代码（无需长篇证明）证明相同的属性。
- 氛围编码可能导致实现的方案落后当前顶尖水平数十年，因为大语言模型不会建议已有的解决方案。