Evergreen обещает язык для системного кода, безопасность которого доказывает компилятор
Evergreen: A Provably Safe Systems Language
Новый язык Evergreen объединяет явные контракты, проверяемые инварианты и ручное управление памятью: предусловия, постусловия и инварианты данных записываются рядом с кодом и становятся обязательствами для компилятора. Он отслеживает время жизни участков памяти и оставшиеся допустимые ссылки, а доказательства и вычисления на этапе проверки стираются, не влияя на производительность. Авторы заявляют, что язык мощнее C и безопаснее Rust.
Запишите, что должно выполняться. Пусть компилятор проверит, что это выполняется.