Po letech vývoje byla vydána verze 4 RC (release candidate) jazyka Lean od Microsoft Research. Jde o čistě funkcionální jazyk s unikátní efektivní a plně automatickou správou paměti („functional but in-place“) založenou na počítání referencí.
Starší verze jazyka se zaměřovaly zejména na matematiky, Lean nebyl plnohodnotný jazyk, ale nástroj pro formalizaci důkazů. Nová verze (Lean 4) se snaží být podle autorů univerzálním funkcionálním jazykem založeným na moderních funkcionálních konstrukcích pro typovou kontrolu, správu paměti a zdánlivě imperativní kód („do unchained“).
Překladač je napsán převážně v Leanu samotném. Kód se překládá do jazyka C, je proto velmi jednoduché volat z Leanu nativní knihovny. Typový systém jazyka umožňuje provádět formální verifikaci programů a garantuje absenci běhových chyb v přeloženém kódu.
ČLÁNKY DO MAILU