Jag arbetar på Concrete v2-specifikationen. Den första versionen har redan fungerande kod och vi lärde oss mycket genom att implementera den. Nu har jag lagt till några nya intressanta funktioner som kommer från Zig, Austral, Lean/Coq. Jag designar ett systemspråk kring formell verifiering från början med några intressanta funktioner. Funktioner: - kärna formaliserad i Lean 4 - linjära typer (Austral-stil, inte Rusts affine) - lån utan livstidsannoteringar - möjligheter för effektspårning - allokator godkänd som kapabilitet (Zig-stil) - ren som standard - ! för orena funktioner (från Roc) Hur de komponerar: Linjära typer är grunden. Varje värde konsumeras exakt en gång. Inga läckor, ingen dubbel fri, ingen användning efter frigörelse. Minnessäkerhet utan GC. Den är mer ordrik men mer konkret och tydlig än affina typer. Att låna gör linjäritet användbart. Referera tillfälligt till ett värde utan att konsumera det. Lexikala regioner istället för Rusts livstidsannoteringar. Kompilatorn drar slutsatser om vad Rust får dig att skriva. Kapabiliteter spårar effekter. En funktion som läser filer deklarerar det. En funktion som allokerar deklarerar den. Ingen deklaration betyder inga effekter, garanterat. grep with(Network) hittar varje funktion som rör nätverket. Allokatorn som förmåga gör allokeringen synlig. Kod utan with(Alloc) rör bevisligen aldrig högen. Du styr vilken allokator som betjänar vilken kodväg. Arena, pool, stackallokering, allt explicit. Pure inverterar som standard den vanliga modellen. Effekter kräver deklaration. Det vanliga fallet (ren beräkning) behöver ingen annotation. Lean-kärnan binder ihop det. När kompilatorn säger att ditt program är säkert, stöds det påståendet av bevis.