Evergreen, un nou llenguatge de sistemes que vol demostrar formalment la seguretat del codi
El llenguatge permet escriure precondicions, postcondicions i invariants al costat del codi perquè el compilador els verifiqui, i també controla la memòria amb propietat i referències com Rust. Les demostracions s'esborren després de la verificació i no afecten el rendiment. L'eslògan promet ser «més potent que C i més segur que Rust».
Evergreen és un llenguatge de programació de sistemes que combina contractes explícits, invariants verificats i control directe de la memòria. La idea és que el programador escrigui què ha de complir-se, com ara que un valor no sigui mai zero o que una suma no desbordi, i que el compilador comprovi que el codi ho respecta.
Pel que fa a la memòria, el llenguatge treballa amb disposicions explícites de les dades, propietat i referències prestades, i fa un seguiment de quan una zona de memòria és viva i de quins usos continuen sent vàlids. Les demostracions, els lemes per inducció i els càlculs «ideals» amb enters matemàtics s'eliminen després de la verificació, de manera que el codi executable només conserva la feina necessària.
El web inclou un entorn de proves que executa el compilador al navegador amb WebAssembly i un enllaç al codi font. Les interaccions amb l'exterior, com la consola, es marquen com a supòsits explícits que el compilador no pot verificar. De moment, les promeses de superar C i Rust són l'eslògan del projecte, no un resultat contrastat.