Evergreen: A Provably Safe Systems Language

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 }