一篇技术观点文章提出，随着人工智能编程从简单的“提示即生成”发展为拥有验证框架、规则文件、测试套件和自主执行流程的工程实践，软件工程的重点正在改变。作者认为，当人类越来越少逐行阅读AI生成的代码时，编程语言的核心价值就不再只是便于人类阅读实现细节，而是要更精确地表达“程序应该做什么”。因此，未来语言的竞争力可能会从实现便利性转向规格表达能力。

文章以Lean 4为例，主张用类型系统直接充当规格说明。其理论基础是Curry-Howard对应关系：类型即命题，程序即证明。依赖类型让开发者不仅声明某个函数返回列表，还可以要求它返回一个附带机器可验证排序证明的有序列表。这样，编译器不再只检查代码能否运行，而是检查实现是否满足逻辑承诺。只要规格可以写成类型，AI就可以自由选择算法，但若没有有效证明，结果会被编译器拒绝。

作者认为，这标志着类型驱动开发可能迎来新阶段：人类更擅长定义意图和约束，AI更擅长生成实现和补全证明，依赖类型成为两者之间的桥梁。文章通过排序算法的Lean 4示例说明，无论是插入排序还是其他AI生成的实现，类型本身都能强制输出满足正确性，而不依赖传统测试作为主要保障。这一观点的核心是，在AI高速生产代码的时代，工程信任的关键应从“看起来能用”转向“可被机器证明”。