Evergreen：一種可證明安全的系統語言
Evergreen: A Provably Safe Systems Language
summary_zh: Evergreen 將明確契約、檢查不變式與記憶體控制整合於單一語言，並由編譯器驗證其安全性。
- 核心特性：Evergreen 透過 explicit contracts 與 checked invariants 讓程式碼自帶前置與後置條件，編譯器在編譯階段即檢查所有不變式。
AI 伴隨問答
針對這篇報導有疑問？可直接點選快捷問題或向 AI 追問背景脈絡與技術細節：
Provably Safe
Systems Code
Evergreen brings explicit contracts, checked invariants, and control over memory into one language. Write down what must hold. Let the compiler check that it does.
nonzero.evg EVERGREEN
type NonZero = usize where self != 0;
impl NonZero {
fn new(x: usize) -> Self
where x != 0
{
NonZero(x)
}
}
fn main() -> usize {
let my_nonzero = NonZero::new(10);
0
}The constructor requires a nonzero input.
The compiler checks the invariant when the value is built.
More Powerful Than C.
Safer than Rust.
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;Playground
EVERGREEN
Console
Ready when you are. Run the example to see its output here.
Loading WebAssembly compiler…Ctrl / ⌘ + Enter to run