Evergreen: A Provably Safe Systems Language

証明可能な安全性

システムコード

Evergreenは、明示的な契約、チェックされた不変条件、およびメモリ制御を1つの言語に統合します。何が満たされなければならないかを記述してください。コンパイラがそれをチェックできるようにします。

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
}

コンストラクタはゼロでない入力を要求します。
コンパイラは値が構築されるときに不変条件をチェックします。

Cよりも強力。

Rustよりも安全。

01 /

不変条件はコード内に存在します。

前提条件、事後条件、およびデータ不変条件を、それらが記述するコードの隣に配置します。それらはコンパイラがチェックする義務となります。

fn increment(n: usize) -> usize
    where n < usize::MAX
    ensures result > n
{
    n + 1
}

02 /

メモリを理解するコンパイラ。

明示的なレイアウト、所有権、および借用参照を扱います。Evergreenは、メモリ領域がいつ有効であるか、およびどの使用が有効であり続けるかを追跡します。

let value: usize = 1;
let cell = &mut value;
*cell = 10;
fact same = value == 10;

03 /

パフォーマンスに影響しない強力な証明。

証明、帰納法による補題、および理想的な計算は、チェック後に消去されます。実行可能なコードは、必要な作業を保持します。

ideal let expected = integer::from(42);
let value: usize = 42;
fact matches =
    integer::from(value) == expected;

例

main.evgEVERGREEN

コンソール

いつでも準備はできています。

例を実行して、その出力をここに表示してください。

Wasmコンパイラをロード中…Ctrl / ⌘ + Enter で実行

---