Я работаю над спецификацией Concrete v2. Первая версия уже имеет рабочий код, и мы многому научились, реализуя его. Теперь я добавил несколько новых интересных функций, которые пришли из Zig, Austral, Lean/Coq. Я разрабатываю языки системного программирования с акцентом на формальную верификацию с самого начала с некоторыми интересными функциями. Функции: - ядро, формализованное в Lean 4 - линейные типы (в стиле Austral, а не аффинные Rust) - заимствование без аннотаций времени жизни - возможности для отслеживания эффектов - аллокатор передается как возможность (в стиле Zig) - по умолчанию чистый - ! для нечистых функций (из Roc) Как они компонуются: Линейные типы являются основой. Каждое значение потребляется ровно один раз. Нет утечек, нет двойного освобождения, нет использования после освобождения. Безопасность памяти без сборщика мусора. Это более многословно, но более конкретно и ясно, чем аффинные типы. Заимствование делает линейность удобной. Временно ссылается на значение, не потребляя его. Лексические области вместо аннотаций времени жизни Rust. Компилятор выводит то, что Rust заставляет вас писать. Возможности отслеживают эффекты. Функция, которая читает файлы, объявляет это. Функция, которая выделяет память, объявляет это. Отсутствие объявления означает отсутствие эффектов, гарантировано. grep с(Network) находит каждую функцию, которая касается сети. Аллокатор как возможность делает выделение памяти видимым. Код без with(Alloc) доказуемо никогда не касается кучи. Вы контролируете, какой аллокатор обслуживает какой путь кода. Арена, пул, стековое выделение, все явно. Чистый по умолчанию инвертирует обычную модель. Эффекты требуют объявления. Общий случай (чистые вычисления) не требует аннотации. Ядро Lean связывает это все вместе. Когда компилятор говорит, что ваша программа безопасна, это утверждение подтверждается доказательством.