Pracuję nad specyfikacją Concrete v2. Pierwsza wersja ma już działający kod i wiele się nauczyliśmy, implementując ją. Teraz dodałem kilka nowych interesujących funkcji, które pochodzą z Zig, Austral, Lean/Coq. Projektuję język systemowy oparty na formalnej weryfikacji od samego początku z interesującymi funkcjami. Funkcje: - jądro sformalizowane w Lean 4 - typy liniowe (w stylu Austral, nie affine Rust) - pożyczanie bez adnotacji czasu życia - możliwości śledzenia efektów - alokator przekazywany jako możliwość (w stylu Zig) - domyślnie czysty - ! dla funkcji nieczystych (z Roc) Jak się komponują: Typy liniowe są fundamentem. Każda wartość konsumowana dokładnie raz. Brak wycieków, brak podwójnego zwolnienia, brak użycia po zwolnieniu. Bezpieczeństwo pamięci bez GC. Jest bardziej rozbudowane, ale bardziej konkretne i jasne niż typy affine. Pożyczanie sprawia, że liniowość jest użyteczna. Tymczasowe odniesienie do wartości bez jej konsumowania. Regiony leksykalne zamiast adnotacji czasu życia Rust. Kompilator wnioskował to, co Rust każe ci pisać. Możliwości śledzą efekty. Funkcja, która odczytuje pliki, deklaruje to. Funkcja, która alokuje, deklaruje to. Brak deklaracji oznacza brak efektów, gwarantowane. grep with(Network) znajduje każdą funkcję, która dotyka sieci. Alokator jako możliwość sprawia, że alokacja jest widoczna. Kod bez with(Alloc) dowodowo nigdy nie dotyka sterty. Kontrolujesz, który alokator obsługuje którą ścieżkę kodu. Arena, alokacja w puli, alokacja na stosie, wszystko jawne. Domyślnie czysty odwraca zwykły model. Efekty wymagają deklaracji. Typowy przypadek (czysta obliczenia) nie potrzebuje adnotacji. Jądro Lean łączy to wszystko. Kiedy kompilator mówi, że twój program jest bezpieczny, to twierdzenie jest poparte dowodem.