编程语言

AI 写实现，人和编译器共同验证意图。

专为 vibe coding 设计的 AI 协同编程语言。

每个对外可见的函数必须携带 spec。spec 是唯一真相源——意图本身也是被验证的对象。

打开 Playground 阅读规格书

fn max(a: Int, b: Int) -> Int
  spec {
    post result >= a && result >= b
    examples { max(1, 2) == 2 }
  }
{ if a >= b { a } else { b } }

核心不变量

三条规则，编译期强制

可见函数必须有 spec

每个对外可见的函数在定义处声明前置条件、后置条件与样例；没有 spec 的公开函数无法通过编译。

spec 是唯一真相源

文档、注释、测试都不再各自为政——需求就写在代码旁边，并且可被执行。

spec 本身也被验证

编译器同时检查：实现满足 spec，且 spec 非空洞、不矛盾、样例可达。

示例

意图写进代码

fn max(a: Int, b: Int) -> Int spec { post result >= a post result >= b post result == a || result == b examples { max(1, 2) == 2 max(5, 5) == 5 max(0, -3) == 0 } } { if a >= b { a } else { b } }

在 Playground 中继续编辑 →

路线图

状态：M1–M5 全部完成