Ich arbeite an der Concrete v2-Spezifikation. Die erste Version hat bereits funktionierenden Code und wir haben viel gelernt, indem wir sie implementiert haben. Jetzt habe ich einige neue interessante Funktionen hinzugefügt, die aus Zig, Austral, Lean/Coq stammen. Ich entwerfe eine Systemsprache, die von Anfang an auf formale Verifikation ausgerichtet ist, mit einigen interessanten Funktionen. Funktionen: - Kernel in Lean 4 formalisiert - lineare Typen (im Austral-Stil, nicht Rusts affine Typen) - Ausleihen ohne Lebensdauer-Anmerkungen - Fähigkeiten zur Effektverfolgung - Allokator als Fähigkeit übergeben (im Zig-Stil) - standardmäßig rein - ! für unreine Funktionen (aus Roc) Wie sie zusammenspielen: Lineare Typen sind die Grundlage. Jeder Wert wird genau einmal konsumiert. Keine Lecks, kein doppeltes Freigeben, keine Nutzung nach Freigabe. Speichersicherheit ohne GC. Es ist ausführlicher, aber konkreter und klarer als affine Typen. Das Ausleihen macht Linearität nutzbar. Temporär auf einen Wert verweisen, ohne ihn zu konsumieren. Lexikalische Regionen anstelle von Rusts Lebensdauer-Anmerkungen. Der Compiler schließt, was Rust dich schreiben lässt. Fähigkeiten verfolgen Effekte. Eine Funktion, die Dateien liest, erklärt dies. Eine Funktion, die allokiert, erklärt dies. Keine Erklärung bedeutet keine Effekte, garantiert. grep mit(Network) findet jede Funktion, die das Netzwerk berührt. Allokator als Fähigkeit macht die Allokation sichtbar. Code ohne with(Alloc) berührt nachweislich niemals den Heap. Du kontrollierst, welcher Allokator welchen Codepfad bedient. Arena-, Pool-, Stapelallokation, alles explizit. Rein standardmäßig kehrt das übliche Modell um. Effekte erfordern eine Erklärung. Der häufigste Fall (reine Berechnung) benötigt keine Anmerkung. Der Lean-Kernel verbindet alles. Wenn der Compiler sagt, dein Programm ist sicher, wird diese Behauptung durch einen Beweis untermauert.