Sto lavorando sulla specifica Concrete v2. La prima versione ha già un codice funzionante e abbiamo imparato molto implementandola. Ora ho aggiunto alcune nuove funzionalità interessanti che provengono da Zig, Austral, Lean/Coq. Sto progettando un linguaggio di sistemi attorno alla verifica formale fin dall'inizio con alcune funzionalità interessanti. Funzionalità: - kernel formalizzato in Lean 4 - tipi lineari (stile Austral, non affine di Rust) - prestiti senza annotazioni di durata - capacità per il tracciamento degli effetti - allocatore passato come capacità (stile Zig) - puro per impostazione predefinita - ! per funzioni impure (da Roc) Come si compongono: I tipi lineari sono la base. Ogni valore consumato esattamente una volta. Nessuna perdita, nessun doppio rilascio, nessun uso dopo il rilascio. Sicurezza della memoria senza GC. È più verboso ma più concreto e chiaro rispetto ai tipi affini. Il prestito rende la linearità utilizzabile. Riferire temporaneamente a un valore senza consumarlo. Regioni lessicali invece delle annotazioni di durata di Rust. Il compilatore inferisce ciò che Rust ti costringe a scrivere. Le capacità tracciano gli effetti. Una funzione che legge file lo dichiara. Una funzione che alloca lo dichiara. Nessuna dichiarazione significa nessun effetto, garantito. grep con(Network) trova ogni funzione che tocca la rete. L'allocatore come capacità rende l'allocazione visibile. Il codice senza with(Alloc) non tocca mai provabilmente l'heap. Controlli quale allocatore serve quale percorso di codice. Arena, pool, allocazione stack, tutto esplicito. Puro per impostazione predefinita inverte il modello abituale. Gli effetti richiedono dichiarazione. Il caso comune (computazione pura) non ha bisogno di annotazione. Il kernel Lean unisce il tutto. Quando il compilatore dice che il tuo programma è sicuro, quella affermazione è supportata da una prova.