Evergreen: A Provably Safe Systems Language

109 points by jordan_bonecut 20 hours ago on hackernews | 87 comments

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

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

Console

Ready when you are.

Run the example to see its output here.

Loading WebAssembly compiler…Ctrl / ⌘ + Enter to run

