1 分•作者: jasisz•5 个月前
我一直在围绕一个简单的问题构建 Aver：
如果 AI 将编写更多初稿，那么人类评审者的来源应该是什么样子的？
Aver 是一种实验性的静态类型语言和工具链，用于 AI 编写、人类评审的代码。
我的看法是，源代码应该包含比实现更多的内容。在大多数项目中，实现存在于代码中，但意图存在于文档中，决策存在于 ADR 或工单中，预期行为存在于测试中，这些测试可能与它们所描述的内容保持一致，也可能不一致。
Aver 尝试将这些部分作为一等公民：
* 函数签名中显式的、方法级别的副作用
* 用于机器可读函数意图的 `?` 字符串
* 用于设计选择和权衡的 `decision` 块
* 用于纯函数的并置 `verify` 块
* 用于 effectful 流程的确定性记录/回放
* 用于紧凑的合约级模块导出的 `aver context`
* 编译到 Rust 的 `aver compile`
* 证明纯子集的机械证明检查的 `aver proof` 到 Lean 4
一个小型的纯函数示例：
```
fn charge(account: String, amount: Int) -> Result<String, String>
? "纯粹的费用验证和交易 ID 创建。"
match amount
0 -> Result.Err("不能收取零费用")
_ -> Result.Ok("txn-{account}-{amount}")
verify charge
charge("alice", 100) => Result.Ok("txn-alice-100")
charge("bob", 0) => Result.Err("不能收取零费用")
```
评审者可以一目了然地看到该函数的作用（`?`）以及机器可检查的预期行为示例（`verify`）。
一个 effectful 包装器看起来像这样：
```
fn chargeAndPrint(account: String, amount: Int) -> Result<Unit, String>
? "围绕 charge 的 effectful 包装器。"
"成功时打印交易 ID。"
! [Console.print]
result = charge(account, amount)
match result
Result.Ok(txn) ->
Console.print(txn)
Result.Ok(())
Result.Err(err) ->
Result.Err(err)
```
`!` 使副作用成为签名的一部分，而不是隐藏在实现内部。
Aver 故意具有主观性：没有异常，没有 null，没有 `if`/`else`，没有循环，没有闭包。分支通过 `match`，失败通过 `Result`，缺失通过 `Option`，副作用是显式的。
该仓库包含小型示例，但也包含 `projects/workflow_engine`，这是我尝试构建的中型可审计应用程序核心，具有 app/domain/infra 分割、可重放的 effectful 流程以及 verify 驱动的纯逻辑。
这还处于早期阶段。我并没有声称每个人都应该用 Aver 替换主流语言。
我正在测试的更狭窄的问题是，将意图、决策、检查和 effect 边界在源代码中实现机器可读性，是否能使 AI 生成的代码更容易评审、约束和信任。
我特别希望收到关于这是否感觉像一种值得存在的语言的反馈，或者同样的想法是否应该仅仅是基于现有语言的约定和工具。