C*: программирование и верификация на одном языке
C*: Unifying Programming and Verification in C
Исследователи представили C* — расширение языка C, которое встраивает доказательства прямо в код. Благодаря символьному исполнению и LCF-ядру программисты могут проверять свои программы в реальном времени, не покидая привычную среду. C* объединяет реализацию и верификацию, используя C как общий язык, что упрощает разработку и сопровождение безопасного системного ПО. Прототип успешно проверен на наборе небольших C-программ и реальном кейсе — функции attach аллокатора pKVM.
C* объединяет разработку кода реализации и кода доказательства, используя C в качестве общего языка.
- eggy
Я уже давно на этой лошади. Я остановился на изучении Ada/SPARK. Ada 2022 начнёт подпитывать новое обновление SPARK 2014. Да, они оба многословны, если вам такое не нравится, и не нравится синтаксис в стиле Паскаля. Поверьте, мне нравятся APL/J/k/uiua/BQN, Forth и ASM. Обычно я безразличен к синтаксису, если язык и экосистема (важнее, чем многие думают) удовлетворяют вашим потребностям. Я пробовал Rust ещё в 2018, а затем снова в 2023, но нашёл его очень сложным и, ладно, я не фанат его синтаксиса. Я бы предпочёл что-то более похожее на ML или Haskell. Zig казался неплохим, но другой вариант использования, и слишком новый. В конце концов, Ada/SPARK десятилетиями используются в огромных, высоконадёжных и высокобезопасных приложениях. Rust получает часть их любви, и наоборот. AdaCore создала верифицированный компилятор Rust, но с реальным продуктом (тельфер Blacktail) в разработке нам нужен набор инструментов, гарантии и лёгкость аудита и приёмки для достижения высокой безопасности и сертификации по стандартам. Подумайте об аэрокосмической отрасли, обороне, железных дорогах и автомобилестроении. Я начал программировать в 1977, так что в моём сердце всегда есть место для ASM/C. Я игрался с F#, F* и LOW от Microsoft, они хороши, но у них, как и у Rust, просто нет реального наследия Ada/SPARK. Я использую Shen для написания некоторых формально верифицированных моделей менее критичных к безопасности областей нашего ПО, и это освежает, однако моя основная работа — сосредоточиться на Ada/SPARK, пока Rust не созреет больше с формально верифицированным и доказанным...
- IsTom
Мне нравится концепция логики разделения не меньше, чем любому другому, но я не думаю, что это оно. Просто посмотрите на примеры: одни только инварианты циклов длиннее всего примера. Это проблема не только эргономики, но и оставляет много места для ошибок в спецификациях. И я подозреваю, что пересечение людей, пишущих на C, которые вы хотите верифицировать, с людьми, занимающимися формальной верификацией, не особенно велико.
- gavinray
Я действительно думаю, что языки, учитывающие верификацию, станут необходимостью. Недавно немного написал об этом: https://gavinray97.github.io/blog/design-by-contract-and-eff...
- Taikonerd
Авторы упоминают это, но просто чтобы отметить: это звучит как F*, ещё один язык, ориентированный на доказательства. (https://fstar-lang.org/) F* принадлежит семейству языков ML, поэтому он выглядит совсем иначе, чем C*.
- slowcache
Я думаю, что формальная верификация — очень интересная область, но для меня это неприемлемо, потому что у меня на клавиатуре нет перевёрнутой E.