Evergreen、コンパイラが安全性を証明するシステム言語を発表

Evergreen: A Provably Safe Systems Language

Evergreenは、事前条件・事後条件・データ不変条件をコードのそばに書き、コンパイラにその成立を検証させるシステム言語。明示的なメモリレイアウトや所有権、借用参照を扱い、メモリ領域が有効な期間と有効な使用を追跡する。証明や帰納法による補題、理想計算は検査後に消去されるため、実行性能には影響しない。