Evergreen — проект системного языка программирования, в котором предусловия, постусловия и инварианты данных записываются рядом с кодом. Компилятор превращает эти утверждения в обязательства, которые необходимо проверить. Идея состоит в том, чтобы программист явно указывал свойства, обязательные для корректной работы, а не оставлял их только в документации или комментариях.
На демонстрационном сайте показан тип NonZero на основе usize с инвариантом self != 0. Его конструктор принимает число только при условии x != 0, поэтому созданное значение должно сохранять ненулевое состояние. Другой пример описывает функцию increment: предусловие требует, чтобы аргумент был меньше usize::MAX, а постусловие гарантирует, что результат больше исходного числа. Так компилятор получает формальное основание для проверки сложения без переполнения.
Отдельное направление Evergreen — контроль памяти. Язык предусматривает явные размещения данных, владение и заимствованные ссылки. Компилятор отслеживает, когда область памяти остаётся действительной и какие обращения к ней допустимы. В примере изменяемая ссылка используется для записи значения, а конструкция fact фиксирует ожидаемое состояние после присваивания.
Доказательства, леммы по индукции и так называемые идеальные вычисления не должны увеличивать стоимость готовой программы. После проверки они стираются: исполняемый код сохраняет только операции, необходимые для работы. Например, значение можно сравнить с идеальным математическим представлением числа, не превращая эту проверку в дополнительные действия во время выполнения.
Авторы используют громкий тезис «мощнее C, безопаснее Rust», но это позиционирование проекта, а не подтверждённый на сайте сравнительный результат. Представленные материалы описывают механизмы языка и небольшие примеры, а не независимые тесты производительности или безопасности. Сайт также предлагает запустить демонстрацию через компилятор WebAssembly прямо в браузере. Практический смысл подхода — совместить низкоуровневый контроль с машинно проверяемыми свойствами программы и при этом не оставлять доказательную часть в итоговом машинном коде.