我正在开发一门语言，让 AI 编写的代码更安全。

01 — 为什么要做

我已经读不完智能体写的所有代码了。

现在，我的很多代码都由 AI 智能体编写。我想，很快会有很多人也处于这种状态，而代码审查跟不上这样的规模。

所以，我想要一门语言，让安全更多地依靠编译器，而不是依靠某个人仔细阅读。对于不是自己写的代码，我也需要一些可以依赖的保障。

我觉得，Rust 是你会希望 AI 使用的语言。但坦白说，我并不擅长 Rust，也一直没能习惯所有权。Almide 是我的一次尝试：保留那样的安全性，却不让任何人或智能体手写所有权相关的部分。

它采用静态类型，通过 Rust 编译为原生代码，也能直接生成 WebAssembly。它提供 Option 和 Result、穷尽模式匹配，以及显式的副作用声明。

02 — 不必手写，就少一处出错

所有权不用你写，由编译器推断。

type Order = { id: Int, items: List[String], total: Int }

fn large(orders: List[Order]) -> List[Order] =
  orders |> list.filter((o) => o.total > 500)

fn main() -> Unit = {
  let orders: List[Order] = [
    { id: 1, items: ["pen", "ink"], total: 260 },
    { id: 2, items: ["desk"], total: 900 },
  ]
  let big = large(orders)
  println("${list.len(orders)} orders, ${list.len(big)} large")
  for o in orders {
    println("${o.id}: ${list.join(o.items, ", ")}")
  }
}

$ almide run orders.almd --target wasm
2 orders, 1 large
1: pen, ink
2: desk

orders 被传给 large，之后又在循环中使用。源码没有标明移动、借用或复制，没有生命周期，也没有 free。

编译器通过 Perceus 风格的推断，确定每个堆上的值在何处创建、共享和消耗。两个目标平台采用不同方式执行这些操作：原生目标输出 Rust，由 Rust 自身的 drop 负责释放；Wasm 使用引用计数。

03 — 我最在意的部分

编译器不能给自己的工作打分。

我不信任自己写的编译器。它是我借助 AI 智能体开发的，我凭什么信任它？

每次构建 Wasm 时，编译器都必须记录自己做过什么，并给出证据：每一处值的共享或释放，每一次数组索引检查。另一个独立程序读取这些证据。如果证据不成立，就不生成输出文件。

被拒绝不是你的代码有 bug，而是编译器出了问题。构建信息会明确说明：

error[certificate-rejected]: app.almd: almide-verify judged this build's
certificate and did not accept it (exit 1)
  app.wasm was not written: the build's own certificate does not hold,
  which is a compiler bug — please report it

已节选。验证器自己的报告接在第一行之后。

04 — TRUST SPINE

检查器也会有 bug，所以一共有四个。

只有一个检查器，只是把信任转移到了别处。这四个检查器以不同方式构建，同一个错误同时出现在四者中的可能性因此较低。项目把它们与所检查的证据统称为 Trust Spine。

在 CI 中，Proofcore、Proofcast 和 Buildgate 必须对测试集每个程序的每一条证据给出一致的判定。这套机制的一次拒绝，已经在我的编译器中发现过真实的错误编译。

仓库中的证明由 46 个 Rocq 文件构成，约 21,700 行，包含 654 条定理和引理。证明针对检查器及其模型，而不是编译器。

证据证明什么

证据按性质分类，每种性质对应一类证据。每类都有自己的规则，四个检查器应用的就是这些规则。

这些性质适用于证据覆盖的代码。Byteanchor 将边界、初始化和字段事件与字节重新核对，并把记录的引用计数事件与文件中的调用匹配。无法与指令对应的事件会被计为未定位，而不会悄悄通过。

05 — 代码出错时

错误信息会告诉智能体该改哪里。

智能体会犯错，重要的是接下来怎么办。学过其他语言的智能体可能会写出 items.length：

error[E013]: no field 'length' on list
  --> app.almd:3:14
  in field access .length
  here: println("${items.length}")
  hint: Almide values have no fields — use the `list` stdlib module.
  try: (machine-applicable — `almide fix` applies it)
      list.len(items)

$ almide fix app.almd
  Applied 1 machine-applicable fix-it(s) from diagnostics: E013 at line 3

这种修复是机械性的，因此工具会直接应用。函数名拼写错误则不同：

error[E002]: undefined function 'string.lenn'
  hint: Did you mean `string.len`?

$ almide fix app.almd
1 diagnostic(s) have `try:` snippets that need manual application:
  [E002] app.almd:3:14  undefined function 'string.lenn' (maybe-incorrect)

0.69.0 版本的编译器输出，已节选。

这涉及对作者意图的猜测，所以只保留为建议。我希望工具能清楚区分机械性修复与对意图的判断。

06 — 不让错误进入成品

遗漏分支会导致编译错误，忽略失败也是。

我最常见到的智能体修改错误是：给类型增加一个变体，却漏掉某个必须处理它的位置。

type Shape =
  | Circle(Float)
  | Rect(Float, Float)
  | Triangle(Float, Float)      // added

fn area(s: Shape) -> Float = match s {
  Circle(r) => 3.14159 * r * r,
  Rect(w, h) => w * h,
}                               // not updated

error[E010]: non-exhaustive match: missing Triangle(_, _)
  --> shape.almd:6:36
  hint: add arms for Triangle(_, _):
  Triangle(arg1, arg2) => _

失败也是如此。可能失败的调用会返回 Result，你必须说明如何处理它。直接丢弃它是错误，不是警告。

effect fn load(path: String) -> String = {
  let text = fs.read_text(path)     // can fail, and nothing says so
  text
}

error[E041]: implicit propagation of this binding's value was removed —
this value is a Result
  --> load.almd:4:14
  hint: Write `expr!` to propagate, or consume the Result as a value
  (`??`, `?`, match ok/err).

0.69.0 版本的编译器输出，已节选。

加一个字符就能修复：fs.read_text(path)!。关键在于，作者必须作出决定，而且这个决定在源码中清晰可见。

07 — 一份源码，两个目标

同一份源码生成原生程序和 WebAssembly，要求输出一致。

原生构建通过 Rust 完成。WebAssembly 由编译器直接生成，中间不经过 LLVM。Hello world 生成的是一个 325 字节的 .wasm 文件。

两个后端可能产生不同结果。因此，每一项可观察行为的承诺都记录为契约，目前共有 454 项，每项都关联可执行的证据。CI 在两个目标上运行 1,055 个程序，比较 stdout、stderr 和退出码。第三个执行器也参与核对：它是一个在生成任何代码之前就运行程序的解释器。

比较在文档规定的条件下成立。随机性、时钟和平台细节各有明确限定范围的契约；解释器对其无法运行的 17 个程序不参与判定。

08 — 还有什么

这是一门完整的语言，不是演示。

09 — 尚未完成的部分

它还没完成，我想把这一点说清楚。

• 编译器整体未经形式化证明。证明覆盖检查器及其模型。
• 原生构建不会运行验证器。它们通过经过认证的渲染器构建，如今整个测试集也都走这条路径。但证据在项目验证中判断，不在你的构建中判断；渲染器无法处理的程序仍会回退到标准代码生成器。
• 四个检查器中，只有一个在你的电脑上运行。另外三个在 CI 中针对测试集运行。如果没有安装验证器，Wasm 构建会未经检查而完成。
• 部分证据并不完整。只覆盖程序一部分的证书也会放行。Component 输出不采用这种方式检查。
• 并非每个记录的事件都已与指令关联。Byteanchor 将无法定位的事件报告为未定位。这个数字并非处处为零。
• 程序可以通过所有检查，却仍然算出错误的结果。这些检查都不判断逻辑是否正确。
• 我无法证明智能体写 Almide 比写 Rust 或 TypeScript 更好。我第一次测量时，强模型在每种语言上都接近 100%，所以结果无法说明问题。
• 目前仍是 pre-1.0。存在已知 bug，也还会发生变化。

哪些已经证明、哪些只是被信任，完整说明在仓库中：已证明与受信任的部分。

10 — 如何开发

我用 AI 智能体开发了它。这正是重点。

编译器用 Rust 编写，开发时我大量使用了 AI 智能体。我先把这件事说清楚，因为有些人不想看以这种方式开发的项目，这可以理解。

但这也解释了项目为何设计成这样。如果编译器由智能体编写，我就不能靠“我读过它”来担保它。因此它必须生成证据，再由其他工具检查证据。每个使用智能体的人，都即将在自己的代码上遇到同样的问题。Almide 是我公开探索这个问题的过程。

11 — 试一试

看看它会在哪里出问题。

在线试用环境直接在浏览器中运行，无需安装。在 macOS 或 Linux 上安装编译器和验证器：

curl --proto '=https' --tlsv1.2 -fsSL \
  https://raw.githubusercontent.com/almide/almide/main/tools/install.sh | sh

安装器需要 GitHub CLI（gh）来验证发布证明。Windows 安装及源码构建说明请参见 README。