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.
Try 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.
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
}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;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
1
Ready when you are. Run the example to see its output here.
External console behavior is provided by the host. Evergreen records this boundary as an explicit trustme assumption.