F*: язык программирования, где доказательства встроены в код

На Hacker News обсуждают F* (произносится «эф-стар») — язык программирования общего назначения, ориентированный на доказательства. Его идея в том, что корректность программы проверяется не тестами, а строгим математическим доказательством, встроенным прямо в исходный текст.

Как это устроено

F поддерживает как чисто функциональный, так и «эффектный» стиль программирования. Выразительность ему обеспечивают зависимые типы, а автоматизация доказательств строится на SMT-решателях и тактиках интерактивного доказательства теорем. По умолчанию программы на F компилируются в OCaml, но отдельные фрагменты можно извлекать в F#, C, WebAssembly (инструментом KaRaMeL) или даже в ассемблер через набор Vale. Сам компилятор написан на F* и раскручен через OCaml.

Проект распространяется под лицензией Apache 2.0, открыт на GitHub и активно развивается силами Microsoft Research, Inria и сообщества. Есть готовые сборки под Windows, Linux и macOS, установка через OPAM, Docker и Nix, а также пишущаяся онлайн-книга «Proof-oriented Programming In F*» с примерами, которые можно пробовать прямо в браузере.

Где это уже применяется

Самое интересное, что формально доказанный код на F — не академическое упражнение, а работающие в продакшене компоненты. Вокруг F вырос зонтичный проект Project Everest, посвящённый защищённому взаимодействию. Из него выросла библиотека криптографических примитивов HACL*, доказанные реализации на ассемблере ValeCrypt и объединяющий их провайдер EverCrypt. Этот код используется в браузере Mozilla Firefox, ядре Linux, языке Python, библиотеке mbedTLS, блокчейне Tezos, SDK электронного голосования ElectionGuard и VPN WireGuard.

Отдельного упоминания заслуживает EverParse — генератор разборщиков бинарных форматов, выдающий доказанный корректным C-код. Именно им сгенерированы парсеры в Windows Hyper-V: каждый сетевой пакет, проходящий через облако Azure, сначала разбирается и проверяется кодом из EverParse.

Исследования и ИИ

F остаётся живой темой исследований — от оснований теории типов и эффектов (монады Дейкстры, конкурентная сепарационная логика Steel и Pulse) до приложений в криптографии: верифицированные реализации TLS 1.3, QUIC, протокола Signal, MLS. Есть работы по верификации кода на Rust трансляцией в F, доказанный сборщик мусора для OCaml и верифицированный аллокатор памяти StarMalloc.

Последние годы к F* подступается и машинное обучение: собран датасет из 940 тысяч строк кода и доказательств для обучения моделей автоматическому синтезу доказательств, а агенты 3DGen учатся превращать текстовые спецификации вроде RFC в проверяемые парсеры форматов.

Источник: Hacker News