我正在研究 Concrete v2 规范。第一个版本已经有了可用的代码，我们通过实现它学到了很多东西。现在我添加了一些来自 Zig、Austral、Lean/Coq 的新有趣功能。 我正在设计一个围绕形式验证的系统语言，从一开始就包含一些有趣的特性。 特性： - 在 Lean 4 中形式化的内核 - 线性类型（Austral 风格，而不是 Rust 的 affine） - 无需生命周期注释的借用 - 用于效果跟踪的能力 - 作为能力传递的分配器（Zig 风格） - 默认纯 - ! 表示不纯的函数（来自 Roc） 它们是如何组合的： 线性类型是基础。每个值被消费一次。没有泄漏，没有双重释放，没有使用后释放。没有 GC 的内存安全。它比 affine 类型更冗长，但更具体和清晰。 借用使线性性可用。暂时引用一个值而不消耗它。使用词法区域而不是 Rust 的生命周期注释。编译器推断出 Rust 需要你写的内容。 能力跟踪效果。读取文件的函数声明它。分配的函数声明它。没有声明意味着没有效果，保证如此。使用 grep with(Network) 可以找到每个接触网络的函数。 作为能力的分配器使分配变得可见。没有 with(Alloc) 的代码可以证明永远不会接触堆。你可以控制哪个分配器服务于哪个代码路径。Arena、池、栈分配，全部显式。 默认纯反转了通常的模型。效果需要声明。常见情况（纯计算）不需要注释。 Lean 内核将其结合在一起。当编译器说你的程序是安全的时，这一声明是有证明支持的。