Back Original

Evergreen: A Provably Safe Systems Language

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

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.

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;

Console

Ready when you are.

Run the example to see its output here.

Loading WebAssembly compiler…Ctrl / ⌘ + Enter to run