Ik werk aan de Concrete v2 specificatie. De eerste versie heeft al werkende code en we hebben veel geleerd door het te implementeren. Nu heb ik enkele nieuwe interessante functies toegevoegd die afkomstig zijn van Zig, Austral, Lean/Coq. Ik ontwerp een systeemtaal rond formele verificatie vanaf het begin met enkele interessante functies. Functies: - kernel geformaliseerd in Lean 4 - lineaire types (Austral-stijl, niet Rust's affine) - lenen zonder levensduurannotaties - mogelijkheden voor effecttracking - allocator doorgegeven als mogelijkheid (Zig-stijl) - standaard puur - ! voor onzuivere functies (van Roc) Hoe ze samenkomen: Lineaire types zijn de basis. Elke waarde wordt precies één keer geconsumeerd. Geen lekken, geen dubbele vrijgave, geen gebruik na vrijgave. Geheugensafety zonder GC. Het is meer omslachtig maar concreter en duidelijker dan affine types. Lenen maakt lineariteit bruikbaar. Tijdelijk een waarde refereren zonder deze te consumeren. Lexicale regio's in plaats van Rust's levensduurannotaties. De compiler leidt af wat Rust je laat schrijven. Mogelijkheden volgen effecten. Een functie die bestanden leest, verklaart dit. Een functie die alloceert, verklaart dit. Geen verklaring betekent geen effecten, gegarandeerd. grep met(Network) vindt elke functie die het netwerk aanraakt. Allocator als mogelijkheid maakt allocatie zichtbaar. Code zonder met(Alloc) raakt bewijsmatig nooit de heap. Je controleert welke allocator welke codepad bedient. Arena, pool, stackallocatie, alles expliciet. Puur standaard draait het gebruikelijke model om. Effecten vereisen een verklaring. De gebruikelijke situatie (pure berekening) heeft geen annotatie nodig. De Lean-kernel verbindt het geheel. Wanneer de compiler zegt dat je programma veilig is, wordt die claim ondersteund door bewijs.