2026年的语言得原生支持证明？
thomasahle · x · 2026-07-11
作者提出一个挑衅式观点：**到 2026 年，编程语言如果不原生支持 Lean 证明，就不该再被构建。** 引用内容里提到 Bend2 的卖点： - 编程语言 - CPU 上接近 C 的速度 - GPU 上接近 CUDA 的速度 - 像 JS 一样高层次，支持闭包、对象、递归 - 类 Lean 证明，强迫 AI 写证明以减少 bug 最后作者用“大家都在用”“你愿意付多少钱”来做反问，整体更像是对下一代语言/AI 编程范式的夸张设想。