zhanlang（詹语言）白皮书

版本：v0.1

日期：2026-10-17

本译文仅供参考，以英文版 white-paper.md 为规范。

一句话

zhanlang 是一门面向 vibe coding 的编程语言：AI 写实现，人和编译器共同验证意图——而且意图本身也是被验证的对象。

我们解决什么问题

vibe coding 把人的角色从「编写者」变成「意图提供者与审阅者」。这个转变暴露了一个结构性缺口：AI 生成代码的典型失败模式——幻觉 API、边界错误、与意图漂移——无法在生成过程中被有效拦截。

现有语言的反馈通道（类型系统、测试、运行时断言、文档）全部发生在代码生成之后，且彼此独立维护。一份意图被重复表达四次，就会产生四份漂移。zhanlang 回答一个直觉：如果意图只被表达一次，且这份表达同时是规格、测试、文档与断言，漂移是否就从物理上被消灭了？

第一性原理与设计原则

本语言只服从四条要求，不服从任何「特性拼盘」：

  1. 解决真实问题，不是拼盘。不为「综合各家之长」而堆特性，只解决四份产物漂移这一个问题。
  2. AI 与 vibe coding 优先。把「AI 是主要代码作者、人类提供意图并审阅」当作默认前提。
  3. 第一性原理。先定义不可违反的不变量，再推导语法与工具链；语法和类型都为不变量服务。
  4. 可被他人与 AI 实现。定义是结构化的、可执行验收的，不是散文。

核心不变量

每个对外可见的函数必须携带 spec；spec 是唯一真相源；编译器在构造期同时做两件验证——验证实现满足 spec，验证 spec 本身不是空洞、矛盾或不可达的。

这条不变量的两个半边同样重要：

早期纸面实验的教训已并入设计：spec 表达式必须能谈论状态与副作用（old / modifies / events），否则真实业务意图无法承载。

不是什么

刻意不做的，以避免拼盘：类继承、隐式类型转换、默认动态类型、隐式效果、宏、多分派。每一样被砍掉，都对应一个「别的语言已经有、但与本语言的核心问题无关」的特性。

路线图

里程碑 内容 验收标准
M1 解析与类型检查 文法与类型/效果检查 示例程序全部通过
M2 spec 自检器 非空洞、可达性、样例一致性、引用合法性 构造的空洞/矛盾/不可达 spec 均被拒绝
M3 运行时断言 checked 层级插入断言 违反 spec 的实现在运行期被捕获
M4 静态验证器 verified 层级的最小符号执行（线性/结构化子集 + if 分支展开） max 被静态证明；非线性/递归函数回退 checked
M5 状态词汇 old / modifies / events 的放置规则与运行时语义 示例 03、06 可写且可被检查

每个里程碑都有对应的 conformance 测试，任何实现（不限于官方参考实现）跑通即合格。

与既有工作的关系

zhanlang 不试图发明新的证明理论，而是把成熟构件（契约式设计、效果系统、框架约束、样例蕴含检查）以「spec 自检」为轴重新组合。真正的创新点是那条双半边不变量：历史上工具要么验证实现、要么假设 spec 正确，zhanlang 把「spec 本身会被 AI 写错」当作一等问题来对待。