Jeg jobber med Concrete v2-spesifikasjonen. Den første versjonen har allerede fungerende kode, og vi lærte mye ved å implementere den. Nå har jeg lagt til noen nye interessante funksjoner som kommer fra Zig, Austral, Lean/Coq. Jeg designer et systemspråk rundt formell verifisering fra starten av, med noen interessante funksjoner. Funksjoner: - kjerne formalisert i Lean 4 - lineære typer (Austral-stil, ikke Rusts affine) - lån uten livstidsannotasjoner - muligheter for effektsporing - allokator passert som kapabilitet (Zig-stil) - ren som standard - ! for urene funksjoner (fra Roc) Hvordan de komponerer: Lineære typer er grunnlaget. Hver verdi konsumeres nøyaktig én gang. Ingen lekkasjer, ingen dobbel gratis, ingen bruk etter gratis. Minnesikkerhet uten GC. Den er mer ordrik, men mer konkret og tydelig enn affine typer. Lån gjør linearitet brukbar. Referer midlertidig til en verdi uten å konsumere den. Leksikalske regioner i stedet for Rusts livstidsannotasjoner. Kompilatoren utleder hva Rust får deg til å skrive. Kapabiliteter sporer effekter. En funksjon som leser filer deklarerer det. En funksjon som allokerer, deklarerer det. Ingen erklæring betyr ingen virkninger, garantert. grep with(Network) finner alle funksjoner som berører nettverket. Allokator som kapabilitet gjør allokering synlig. Kode uten with(Alloc) berører beviselig aldri heapen. Du kontrollerer hvilken allokator som serverer hvilken kodesti. Arena, pool, stack-allokering, alt eksplisitt. Pure inverterer som standard den vanlige modellen. Effekter krever erklæring. Det vanlige tilfellet (ren beregning) trenger ingen annotasjon. Lean-kjernen binder det sammen. Når kompilatoren sier at programmet ditt er trygt, støttes den påstanden av bevis.