evergreen

Systems code.
Provably Safe.

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 struct {data: usize} where data != 0;

impl NonZero {
    fn new(x: usize) -> Self
        where x != 0
    {
        return NonZero {data: x};
    }
}

fn main() -> usize {
    let my_nonzero = NonZero::new(10);
    0
}
A checked invariant. NonZero always holds a nonzero value.

The constructor requires a nonzero input.
The compiler checks the invariant when the value is built.

The Core Idea

More intent in the source.
Fewer assumptions in your head.

01 /

Say what must be true.

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

02 /

Keep control of memory.

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

03 /

Carry less into runtime.

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

Playground

The real Evergreen compiler, compiled to WebAssembly. Edit an example, check its proofs, and run the resulting Wasm. Everything happens on your device.

EVERGREEN
Console
Ready when you are.

Run the example to see its output here.
Loading WebAssembly compiler…Ctrl / ⌘ + Enter to run