Lucrez la specificația Concrete v2. Prima versiune are deja cod funcțional și am învățat multe implementându-l. Acum am adăugat câteva funcții noi interesante care vin din Zig, Austral, Lean/Coq. Proiectez de la început un limbaj de sisteme în jurul verificării formale, cu câteva caracteristici interesante. Caracteristici: - nucleu formalizat în Lean 4 - tipuri liniare (stil austral, nu afina lui Rust) - împrumut fără adnotări pe viață - capabilități pentru urmărirea efectelor - alocătorul trecut ca capacitate (stil Zig) - pur implicit - ! pentru funcții impure (din Roc) Cum compun: Tipurile liniare sunt fundația. Fiecare valoare consumată exact o dată. Fără scurgeri, fără dublu gratuit, fără utilizare după gratuit. Siguranța memoriei fără GC. Este mai verbos, dar mai concret și clar decât tipurile afine. Împrumutul face liniaritatea utilizabilă. Referinează temporar o valoare fără să o consumi. Regiuni lexicale în loc de adnotările de viață ale lui Rust. Compilatorul deduce ce te face Rust să scrii. Capabilitățile urmăresc efectele. O funcție care citește fișiere îl declară. O funcție care alocă îl declară. Fără declarație înseamnă fără efecte, garantat. grep with(Network) găsește fiecare funcție care atinge rețeaua. Alocarea ca capacitate face alocarea vizibilă. Codul fără with(Alloc) probabil nu atinge niciodată grămada. Tu controlezi ce alocător servește ce cale de cod. Arenă, pool, alocarea stack-ului, toate explicite. Pur, implicit, inversează modelul obișnuit. Efectele necesită declarație. Cazul comun (calcul pur) nu necesită adnotare. Nucleul Lean leagă totul împreună. Când compilatorul spune că programul tău este sigur, acea afirmație este susținută de dovezi.