当编程语言的设计目标从「让人好读」转向「让机器好写」，整个语言设计的范式都需要重新审视。Vera（v-ERR-a，拉丁语「真理」之意）正是这一理念的产物 —— 它不是传统编程语言的简化版本，而是一种专为大型语言模型（LLM）设计的全新编程语言，其核心理念是「代码不需要正确，只需要可验证」。本文深入分析 Vera 的语言设计决策、编译器架构以及背后的学术依据，探讨机器优先的语言设计思路与工程实现挑战。
从用户到作者：编程语言设计范式的根本转变
编程语言的历史始终与其使用者紧密绑定。汇编语言源于硬件约束，C 语言服务于操作系统开发，Python 则追求人类程序员的生产力提升。每一次语言革新都伴随着使用者需求的变化。然而，当模型逐渐成为代码的主要生成者时，语言设计是否也应该随之调整？Vera 的回答是肯定的。其创始人 Alasdair Allan 在项目文档中指出，当前模型面临的最大问题不是语法，而是「规模化的一致性」—— 模型难以在整个代码库中维护不变量，难以理解修改的连锁反应，难以对状态进行长期推理。它们是模式匹配器，优化的是局部合理性，而非掌握整个系统的架构师。
这一观察得到了实证研究的支持。Wang 等人发表的论文《How Does Naming Affect LLMs on Code Analysis Tasks?》（arXiv:2307.12488）系统地用随机字符串替换变量和函数名，测量 CodeBERT 在代码分析任务上的表现变化。研究发现，良好的命名确实对 LLM 性能有帮助，但 shuffled names（即把名为count的变量与名为result的变量交换）比随机乱码表现更差。模型会被看似合理但错误的名称误导。Le 等人的进一步研究《When Names Disappear》（arXiv:2510.03178）更尖锐地指出，LLM 即使在仅依赖程序结构的执行预测任务中，也会利用标识符与功能之间的统计相关性 —— 这被称为「标识符泄露」。模型表面上理解了代码，实际上只是在熟悉的 token 上进行模式匹配。
这正是 Vera 的理论基础：变量名对 LLM 的帮助实际上是一种拐杖，它让模型看起来理解了代码，而实际上并未进行真正的推理。Vera 的策略是移除这根拐杖，代之以经过验证的结构化信息 —— 类型、合约、效应声明 —— 强制模型站在更坚实的地面上进行推理。
无命名变量的实现：类型化 De Bruijn 索引
Vera 最显著的设计特征是完全没有变量名。所有绑定都通过结构化引用访问：@Int.0表示最近的一个Int绑定，@Int.1表示再往前一个，以此类推。这直接借鉴了 De Bruijn 索引的概念，但 Vera 对其进行 了类型化扩展。每个索引都携带类型信息，编译器可以静态验证每个引用是否解析到正确类型的绑定。
为什么选择这种方式？传统编程语言中，变量名承担了多重职责：标识身份、传达意图、提供文档。而这些职责对 LLM 而言恰恰是负担。模型会混淆不同作用域中同名的变量，会被相似名称误导，还会在大型代码库中丢失名称与值的对应关系。Vera 用结构位置替代名称，让引用本身就是一种约束 ——@Int.0只能是某个Int类型的绑定，类型系统确保它不会指向错误的值。
这种设计在实践中需要配套的工具支持。Vera 提供了--explain-slots选项，可以显示 slot 解析表，帮助开发者（无论是人类还是模型）理解每个@T.n具体对应哪个参数或局部绑定。对于需要人类可读视图的场景，可以在 Vera 之上构建可视化层，根据类型和使用模式推断出人类友好的名称，但这些名称不属于语言本身 —— 语言的规范形式始终是无歧义的。
值得注意的是，De Bruijn 索引在数学上优雅，但在实践中存在「交换操作陷阱」。当表达式涉及交换律运算（如加法、乘法）时，索引可能指向错误的对称操作数。Vera 的文档（DE_BRUJN.md）中详细讨论了这一问题及其解决方案，这也是模型在 VeraBench 基准测试中的主要失败模式。
强制合约系统：Z3 SMT 求解器驱动的静态验证
Vera 的合约系统是其安全网的核心。每个函数必须包含三个声明：requires（前置条件）、ensures（后置条件）和effects（效应声明）。这些不是可选的文档，而是编译器必须验证的硬性约束。以安全除法函数为例：
public fn safe_divide(@Int, @Int -> @Int)
requires(@Int.1 != 0)
ensures(@Int.result == @Int.0 / @Int.1)
effects(pure)
{
@Int.0 / @Int.1
}
编译器会在每个调用点检查前置条件是否满足。对于上述除法，这意味着调用者必须证明除数非零。如果 Z3 能够静态证明合约成立，代码编译通过；如果 Z3 无法判定，则降级为运行时检查。这意味着除以零在 Vera 中不是运行时错误，而是类型错误 —— 合约验证从根本上杜绝了这类常见 bug。
合约系统分为三个层次。第一层是类型系统（机械且完备）：类型检查器验证所有引用解析到正确类型的绑定，函数调用匹配签名，模式匹配穷尽，泛型单态化正确。这一层没有新鲜之处，但它是完备的 —— 只要通过类型检查，组件就能正确组合。第二层是 Z3 合约验证（机械但有界）：编译器将合约翻译为可判定的 SMT 片段，交给 Z3 求解。当前覆盖整数和布尔值的线性运算、数组长度、ADT 构造函数辨别和字段访问，以及结构递归的终止性度量。对于大多数合约，Z3 能够静态验证实现满足规范。无法验证的合约降级为运行时断言。第三层是智能体文档和人类意图（表达性但未验证）：合约本身相对于用户意图是未验证的 ——ensures(@Int.result >= 0)可能不是函数的真正意图。SKILL.md 引导模型写出合理合约，但「合理」没有形式化保证。
这种设计的关键洞察是：人类审计合约而不是实现。合约是小的声明性语句，比散布在实现中的变量名更精确地传达意图。合规审查者只需审计合约（小的声明性语句），无需阅读实现，编译器会证明代码符合这些合约。
代数效应系统：类型安全的副作用追踪
Vera 默认是纯函数式的。执行 IO、网络请求、LLM 推理的函数必须在签名中声明这些效应。调用者必须声明自己允许的完整效应集，才能调用需要这些效应的函数。这创建了一个类型化的安全边界：沙盒模块无法执行其声明的效应集之外的任何操作。
Vera 内置了多种代数效应：<IO>用于标准输入输出，<Http>用于网络请求，<Inference>用于 LLM 推理，<State>用于状态管理，<Exceptions>用于异常处理，<Async>用于异步操作，<Random>用于随机数生成。例如，一个研究主题的函数可能声明为：
public fn research_topic(@String -> @Result<String, String>)
requires(string_length(@String.0) > 0)
ensures(true)
effects(<Http, Inference>)
{
// ...
}
这种效应系统的灵感来自 Koka 语言，但 Vera 将其与合约验证结合。调用者如果只允许<IO>，则无法调用需要<Http>或<Inference>的函数 —— 这种能力分离在类型层面强制执行。对于测试，可以提供模拟处理器而不是发起真实网络请求。
效应系统还支持自定义处理器。Vera 允许为每种效应定义处理函数，拦截并处理效应操作。例如，<Http>效应的处理器可以将真实 HTTP 调用替换为测试桩。这种机制既保证了代码的可测试性，又维持了效应声明的精确性。
编译器架构：七阶段管道的工程实现
Vera 的参考编译器使用 Python 实现，分七个阶段：解析（使用 Lark LALR (1) 语法分析器）、AST 转换、引用解析、类型检查、合约验证（Z3）、WASM 编译、执行。选择 Python 而非更高效的语言是刻意决定 —— 正确性优先于性能。编译器是规范 - faithful 的实现，在快速语言迭代阶段可读性和可测试性比执行速度更重要。
解析阶段使用 Lark 定义 LALR (1) 语法，生成确定性解析器。Vera 的语法故意简洁规范，每种构造只有一种规范形式，减少模型需要学习的表面积。转换阶段将 Lark 的解析树转换为类型化的 AST 节点，每个节点携带类型信息和位置数据。引用解析阶段将@T.n slot 引用解析为具体的绑定。类型检查阶段验证类型正确性、模式匹配穷尽性、泛型单态化。合约验证阶段将 requires 和 ensures 子句翻译为 Z3 可判定的 SMT 公式，调用 Z3 求解器证明或给出反例。WASM 编译阶段将验证后的 AST 翻译为 WebAssembly 字节码。执行阶段使用 wasmtime 运行时在命令行或浏览器中运行程序。
编译器还提供面向模型的错误诊断。传统编译器产生expected token '{'}这样的诊断，而 Vera 产生包含错误位置、错误原因、修复代码示例和规范引用的完整指令。每个诊断都有稳定错误码（E001 到 E702），并可通过--json标志获得结构化 JSON 输出，便于自动化工作流集成。这种设计让模型可以自主理解和修复错误，而不仅仅报告人类可读的诊断信息。
编译目标选择 WebAssembly 有三个原因：便携性（同一.wasm二进制可在命令行或浏览器运行）、沙盒化（WASM 没有环境能力，程序无法执行效应声明不允许的操作）、组件模型（W3C 的 WASM 组件模型支持与 Rust、Go、Python 组件通过 WIT 接口互操作）。
基准测试与实证验证
Vera 项目提供了专门的基准测试 VeraBench，包含 5 个难度级别的 50 个问题，覆盖 6 个模型和 3 个提供商。关键结果：Kimi K2.5 在 Vera 上达到 100% 的 run_correct，超过了 Python 的 86% 和 TypeScript 的 91%。三个模型在 Vera 上超越 TypeScript；旗舰级别平均 93% 的 Vera run_correct 与 93% 的 Python 持平 —— 本质上是平价。这些是单次运行结果，存在高方差；主要失败模式是 De Bruijn slot 排序（@T.n索引排序错误）。
更广泛的文献也支持这些设计选择。Mündler 等人 2025 年 PLDI 论文《Type-Constrained Code Generation with Language Models》发现，在 LLM 代码生成期间强制类型约束使编译错误减少一半以上，功能正确性提高 3.5-4.5%。语法约束 alone 提供的改进有限 —— 是类型约束产生了差异。同一论文发现 94% 的 LLM 生成的编译错误是类型检查失败 —— 这正是强静态类型系统在编译时捕获的错误类别。Sun 等人的《Vericoding》基准测试显示，LLM 在 Dafny 上达到 82% 的验证成功率，而在 Lean 上只有 27%，表明 SMT 自动化验证比显式证明构造更容易被模型处理。
工程权衡与开放挑战
Vera 的设计做了几个重要的工程权衡。首先，Python 编译器在语言迭代阶段便于修改和维护，但如果编译器性能成为瓶颈，需要用 Rust 或 OCaml 重写。Python 参考编译器将作为规范预言机保留。其次，Z3 求解器的表达能力有界 —— 涉及泛型类型参数的合约或跨处理器的符号效应状态建模属于 Z3 无法判定的情形，这些会降级为运行时检查。第三，能力集是固定的（Eq、Ord、Hash、Show），不允许用户定义能力 —— 这是简化语言和避免开放类型类系统一致性问题的有意选择。
当前的已知限制包括：HTTP 仅支持 GET 和 POST，自定义 headers、额外 HTTP 方法、响应状态码、超时和流式传输正在追踪中。LLM 推理支持 Anthropic、OpenAI、Kimi（Moonshot）和 Mistral，通过环境变量配置。泛型特化在某些边界情况下仍有待完善。完整的 13 章形式规范仍在 draft 阶段。
结论与未来方向
Vera 代表了一种新的编程语言设计思路 —— 不是为人类优化可读性，而是为模型优化可验证性。通过消除变量名、强制合约、类型化 De Bruijn 索引和代数效应系统，Vera 创建了一个模型无法偷工减料的环境：它必须写出正确的代码，否则编译器拒绝接受。这种「约束即特征」的设计哲学与传统的「特性即自由」形成鲜明对比。
从编译器工程的角度，Vera 展示了如何将成熟的验证技术（SMT 求解器）与 WebAssembly 编译目标结合，创建一个端到端的可信代码生成管道。七阶段编译器架构清晰分离了关注点，类型检查、合约验证和代码生成各自独立测试和演进。面向模型的错误诊断设计则体现了对自动化工作流的深刻理解。
未来，Vera 路线图上的关键里程碑包括：经过验证的 MCP 工具服务器，合约在编译时保证工具 schema；更广泛的模型评估和纵向跟踪；以及生产级编译器的性能优化。对于编程语言设计领域，Vera 提出了一个根本性问题：当代码的作者不再是人类时，我们的语言设计原则应该怎样改变？至少在目前，答案似乎是：让正确性成为一种结构约束，而不是事后检查。
参考资料
- Vera 项目 GitHub 仓库：https://github.com/aallan/vera
- Wang et al., "How Does Naming Affect LLMs on Code Analysis Tasks?", arXiv:2307.12488
- Le et al., "When Names Disappear: Revealing What LLMs Actually Understand About Code", arXiv:2510.03178
- Mündler, He, Wang et al., "Type-Constrained Code Generation with Language Models", PLDI 2025