Evergreen：把不变量写进类型，让编译器去证明

📋 概述

Evergreen 是一个新系统的语言官网，主张只有一条：把必须成立的条件写下来，让编译器检查它确实成立。语言里有前置条件、后置条件与数据不变量三类契约，写法贴着代码——构造 NonZero 时要求入参非零，编译器在值被构造的地方就检查这条不变量。它同时声称能追踪内存：显式的布局、所有权与借用，编译器记录内存平面何时活着、哪些引用仍然有效。证明部分用 ideal 与 fact 关键字：理想计算与归纳引理在检查后会被擦除，不进入可执行代码，因此作者敢声称「证明不影响性能」。官网还带一个可在线运行的 playground。宣传语是「比 C 更强，比 Rust 更安全」。