编程语言的演进始终与它的使用者紧密相连。汇编语言诞生于硬件约束，C 语言服务于操作系统开发，Python 则回应了人们对生产力的追求。当大语言模型开始成为代码的主要编写者之一时，一个根本性的问题浮现出来：专为人类设计的编程语言，是否真的适合机器生成？
这个问题催生了 Vera—— 一种由 Alasdair Allan 开发的实验性编程语言，其核心理念与传统编程语言截然不同：不是为了让人读懂而设计，而是为了让机器能够正确写出可验证的代码。
设计哲学：从「正确」到「可检验」
传统编程语言的设计假设开发者是人类程序员，语法、命名、文档都是为人可读性服务的。但 Vera 反其道而行之，它的首要目标不是代码的正确性，而是代码的可检验性。
这一设计选择源于对大语言模型弱点的深刻理解。学术研究表明，模型在代码生成中最容易犯的错误并非语法错误，而是与命名相关的错误：选择误导性的变量名、错误地重用名称、丢失名称与值的对应关系。模型本质上是模式匹配器，优化的是局部 plausibility，而非全局架构。
Vera 的设计者提出了一个关键洞察：模型不需要永远正确，它只需要可以被检验。这一理念贯穿了语言的每一个设计决策。
结构引用：消除命名幻觉
Vera 最显著的特征是彻底摒弃了变量名。传统的编程语言依赖有意义的名称来表达意图，而 Vera 采用类型化的 De Bruijn 索引来引用绑定。例如，@Int.0表示最近的一个 Int 类型绑定，@Int.1则表示再往前一个。
这种设计的直接效果是从根本上消除了命名相关的幻觉错误。当模型无法随意创造名称时，整个类别的错误就在语言层面被消除，而不是等到运行时才被发现。结构引用强制模型只能通过类型和位置来访问变量，这是一种约束，但正是这种约束显著降低了模型生成错误代码的概率。
强制合约：第一公民的验证
在 Vera 中，每个函数都必须声明完整的合约，包括前置条件（requires）、后置条件（ensures）和副作用声明（effects）。这不是可选的文档，而是编译器强制执行的语言特性。
以下是一个典型的 Vera 函数签名：
public fn safe_divide(@Int, @Int -> @Int)
requires(@Int.1 != 0)
ensures(@Int.result == @Int.0 / @Int.1)
effects(pure)
{
@Int.0 / @Int.1
}
这个例子展示了 Vera 的核心设计：除零不是运行时错误，而是类型错误。编译器使用 Z3 SMT 求解器在编译时验证实现是否满足合约。如果前置条件不满足，代码甚至无法通过编译。
这种强制合约的方法将验证变成了开发流程的核心部分，而不是事后的测试环节。对于 AI 生成的代码来说，这意味着模型写出的每一行代码都会立即得到反馈，形成「写代码→编译器检查→模型修复」的快速迭代循环。
代数效应：显式副作用管理
Vera 实现了完整的代数效应系统，包括 IO、Http、State、Exceptions、Async、Inference、Random 等七种效应。所有副作用都必须显式声明，纯净（pure）成为默认状态。
对于需要调用大语言模型的函数，Vera 将 Inference 作为一等效应来处理：
public fn classify_sentiment(@String -> @Result<String, String>)
requires(string_length(@String.0) > 0)
ensures(true)
effects(<Inference>)
{
let @String = string_concat("Classify as Positive, Negative, or Neutral: ", @String.0);
Inference.complete(@String.0)
}
这种设计的好处是双重的：副作用被类型系统显式跟踪，使得代码的行为可以被验证；同时 Inference 效应是可模拟的，便于测试和调试。
诊断即指令：面向模型的错误信息
传统编程语言的错误信息往往面向人类开发者，而 Vera 的每一个诊断都附带自然语言解释和具体的修复建议，这些建议是专门为 LLM 设计的。
当函数缺少合约块时，编译器不仅报告错误，还提供完整的修复代码示例。这种设计让模型能够理解问题并直接根据反馈进行修复，形成了机器可读的「写 - 检验 - 修复」闭环。
编译后端：WebAssembly 跨平台
Vera 编译到 WebAssembly，这意味着同一份.wasm文件可以在命令行通过 wasmtime 运行，也可以在浏览器中执行。编译器还支持生成自包含的浏览器绑定包，无需额外的打包工具。
这种设计对于 AI 代码生成特别有意义：模型生成的代码可以直接在任意环境中执行，从服务器到浏览器，实现真正的一次生成，到处运行。
实证结果：VeraBench 基准测试
设计理念需要数据支撑。Vera 团队开发了 VeraBench 基准测试，涵盖 50 个问题，分为五个难度层级：纯算术、代数数据类型、递归、闭包和多函数效应传播。
最新的 v0.0.7 结果显示，在 Kimi K2.5 旗舰模型上，Vera 达到了 100% 的 run_correct 率，超过了 Python 的 86% 和 TypeScript 的 91%。这表明即使没有任何针对 Vera 的训练数据，模型的模式匹配能力也能通过语言的约束性设计得到有效引导。
其他模型的结果则显示了更复杂的图景：GPT-4.1 和 Claude Opus 4 在 Python 和 TypeScript 上的表现仍优于 Vera。这可能反映了这些模型在传统语言上的更深度优化，也说明了 Vera 目前仍处于早期阶段。
值得注意的是，这些结果来自单次运行的 pass@1 评估。稳定的性能评估需要 pass@k 多次采样评估来减少模型的非确定性影响。
设计原则的六点总结
Vera 的设计可以被归纳为六个核心原则：可检验性优先于正确性，显式性优先于便利性，每个构造只有一种规范形式，结构引用优先于命名，合约作为源代码的真理，约束表达力以减少错误机会。这些原则共同构成了一个针对机器生成代码优化的完整语言系统。
局限性与发展阶段
Vera 目前仍处于活跃开发阶段（v0.0.127），其局限性值得关注。首先，强制合约增加了代码编写的初始开销，即使对于简单函数也需要完整的规范。其次，Z3 验证在某些复杂场景下可能超时，需要引导式验证和运行时回退。再次，目前只有 50 个基准问题，需要更大规模的评估来验证设计选择。
此外，Vera 的交易是用人机可读性换机器可检验性。这种设计对于纯机器生成的代码是合理的，但如果代码最终需要人类维护和修改，则可能成为障碍。
未来方向
Vera 代表了一种新的编程语言设计思路：为 AI 原生代而设计的代码。从更广泛的视角来看，它，探索了当代码的主要消费者从人类变成机器时，语言设计应该发生怎样的变化。
编译器的后端适配、WebAssembly 的运行时优化、与现有 CI/CD 系统的集成、以及更大规模的基准测试，都是 Vera 继续发展的方向。更重要的是，它的设计理念为整个编程语言领域提供了一个有趣的思考实验：当约束成为特性，当验证成为默认，机器生成的代码能否达到人类编写代码的可靠性？
资料来源：Vera 官方网站 veralang.dev、GitHub 仓库 github.com/aallan/vera、VeraBench 基准测试结果