Evergreen：一种可证明安全的系统语言

Evergreen：一种可证明安全的系统语言
Evergreen: A Provably Safe Systems Language

01 / 不变量驻留在你的代码中。将前置条件、后置条件和数据不变量放在它们所描述的代码旁。它们会成为编译器检查的义务。fn increment(n: usize) -> usize where n < usize::MAX ensures result > n { n + 1 } 02 / 理解内存的编译器。使用显式布局、所有权和借用引用。Evergreen 会跟踪内存平面何时存活，以及哪些使用仍然有效。let value: usize = 1; let cell = &mut value; *cell = 10; fact same = value == 10; 03 / 不影响性能的强大证明。证明、归纳引理和理想计算在检查后会被擦除。可执行代码保留它需要完成的工作。ideal let expected = integer::from(42); let value: usize = 42; fact matches = integer::from(value) == expected;

Hacker News 上的一篇帖子介绍了可证明安全的系统语言 Evergreen。其创建者表示该语言尚无实用价值，但希望获得反馈，并提到他们正在用 Claude 构建，并进行每日代码审查。一位评论者称赞这一概念，询问证明器提供哪些保证，并警告说语言成功需要社区采用以及强大的互操作性或标准库。创建者回复说，在没有 `trustme` 的情况下，内存不能被作为错误类型寻址，且指针/引用必须在编译时保持存活；用户也可以断言编译器必须证明的事实。他们计划稍后添加标准库。

原文

01 /

Invariants live in your code.

Put preconditions, postconditions, and data invariants beside the code they describe. They become obligations the compiler checks.

fn increment(n: usize) -> usize
    where n < usize::MAX
    ensures result > n
{
    n + 1
}

02 /

A compiler that understands memory.

Work with explicit layouts, ownership, and borrowed references. Evergreen tracks when a memory plane is live and which uses remain valid.

let value: usize = 1;
let cell = &mut value;
*cell = 10;
fact same = value == 10;

03 /

Powerful proofs that don't affect performance.

Proofs, lemmas by induction, and ideal computations are erased after checking. Executable code keeps the work it needs to do.

ideal let expected = integer::from(42);
let value: usize = 42;
fact matches =
    integer::from(value) == expected;

联系我们 contact @ memedata.com