flang: язык, в котором программа обязана доказать, что остановится

Есть класс задач, где неверный ответ дороже отсутствия ответа: расчёт скидки, допуск отгрузки, начисление процентов, проверка права на операцию. Обычный язык такие правила выражает, но ничего про них не обещает. Функция может зациклиться, вернуть не то, потерять случай — и узнаете вы об этом в продакшене.

flang устроен вокруг другого обещания: если функция помечена словом тотальная, компилятор не примет программу, пока не убедится, что эта функция завершается на любом входе. Не проверит на примерах, а выведет из устройства программы. Не вывел — откажет с ошибкой FLANG_NOT_TOTAL, и это ошибка, а не предупреждение, которое можно проглядеть.

Всё написанное ниже проверено на версии 0.7.29 (выпуск 18 октября 2026).

Как выглядит программа

Вот функция подсчёта длины списка из стандартной библиотеки, flang/stdlib/lists.flang:

тотальная функция «Длина» от «А»
  принимает элементы: список «А»
  возвращает число
  обеспечивает «счёт звеньев сходится со встроенной длиной» результат равен (длина элементы)
  пример «Пустой список»
    дано элементы равно пустой список
    ожидается 0
  пример «Три элемента»
    дано элементы равно [7, 8, 9]
    ожидается 3
  пример «Три строки — тем же телом»
    дано элементы равно ["раз", "два", "три"]
    ожидается 3
  свёртка элементы начиная с 0 как акк и эл → акк плюс 1

Здесь пять вещей, которых нет в привычном коде:

Имена в ёлочках. «Длина» — имя из предметной области. Оно может содержать пробелы и писаться по-русски: «Рассчитать скидку», «Проверить право на отгрузку».

Отступы вместо скобок. Тело функции — то, что вложено. У вызова и блока скобок нет.

обеспечивает — постусловие. Утверждение о результате для всех входов. flang check --proof пытается его доказать и пишет, чем доказал; здесь — индукцией по свёртке в теле функции. Утверждение, которое доказать не удалось, названо в отчёте, и flang run такую программу без явного согласия не запустит.

пример — тест внутри функции. Примеры выполняют flang check и flang test; они лежат рядом с кодом, а не в отдельном файле.

от «А» — параметр типа. Одно тело работает и со списком чисел, и со списком строк; третий пример это и проверяет.

Писать можно не только по-русски. Поверхностей слов у языка четыре — русская, английская, эсперанто и китайская, — и все дают одно и то же дерево разбора; как это устроено, разбирает глава «Своя поверхность». Функция из файла docs/examples/rosetta/factorial-english.flang:

total function «Product»
  accepts items: list of number
  returns number
  example «Product of four»
    given items equals [1, 2, 3, 4]
    expected 24
  example «Product of the empty list is one»
    given items equals empty list
    expected 1
  fold items starting with 1 as acc and elem → acc times elem

Ёлочки принадлежат языку, а не раскладке, поэтому имя остаётся в них на любой поверхности. Служебные слова переводятся парами: принимает/accepts, возвращает/returns, обеспечивает/ensures, пример/example, дано/given, ожидается/expected. Полная таблица — docs/site/fspec.md в репозитории. Сообщения компилятора по умолчанию русские на любой поверхности.

Главное решение: два класса программ

Полнота по Тьюрингу и гарантия завершения несовместимы: язык либо выражает любое вычисление, либо про любую его программу можно доказать, что она остановится. Обычно язык выбирает первое и про завершение молчит.

flang делит программы на два класса, и класс проверяет компилятор:

«Структурно меньший аргумент» — хвост списка или строки, поле варианта: то, что заведомо ближе к концу, чем целое. Если рекурсия идёт по неотрицательному числу, которое уменьшается на единицу, это тоже доказывается; для шага посложнее автор называет меру словом убывает, и её убывание проверяется на каждом витке.

Бизнес-правило пишут тотальной функцией и получают гарантию, остальное — обычной. Подробности — в главах «Два класса программ» и «Тотальность».

Что язык делает с побочными эффектами

Чистая функция не читает файлы и не ходит в сеть — иначе про неё ничего нельзя доказать. Но программа, которая ничего не делает во внешнем мире, бесполезна.

В flang действие описывается, а не выполняется: функция возвращает значение-запрос — «прочитать такой файл», «запросить такой адрес», — и остаётся чистой. Исполняет запросы команда flang io, которая передаёт программе ответ среды и получает следующий запрос. План действий — обычное значение: его можно проверить примерами до того, как он коснётся диска или сети. HTTPS работает без внешних программ: клиент TLS 1.3 встроен в двоичный файл.

Что с этим кодом делать дальше

Проверенную программу команда emit переводит на один из десяти языков: C, C++, Go, Rust, Java, JavaScript, TypeScript, Elixir, Python, C#. Получается обычный код на целевом языке со своим рантаймом и сборочным файлом, который дальше живёт в вашем проекте:

$ flang emit скидка.flang --target go --out discount
$ cd discount && go build ./...

Типичный сценарий: правило пишут и проверяют на flang, а в продакшене работает полученный Go или C. Подробнее — в главе «Кодогенерация».

Команды

flang --help перечисляет 15 команд; вот те, что нужны в первый день:

Коды возврата общие: 0 — всё проверено, 1 — не прошло, 2 — неверный вызов, 3 — сделано, но доказано не всё, и недоказанное названо. Реже встречаются 4 (часть проверок пропущена ключом --fast) и 5 (исчерпан предел памяти). Справочник — в главе «Инструмент».

Обычное расширение файла — .flang; принимаются и .fp, .фп, .фланг.

Попробовать за пять минут

Готовая сборка для Linux (x86_64, aarch64) и macOS ставится одной строкой, без компилятора C и без sudo:

curl -fsSL https://raw.githubusercontent.com/digitable-lol/flang/main/install.sh | sh
flang --version        # flang 0.7.29

Скрипт кладёт flang в ~/.local/bin и сверяет архив с SHA256SUMS выпуска. Через Homebrew — brew install digitable-lol/tap/flang-package. Если у вас стоит компилятор Fortran из LLVM, он тоже называется flang: проверьте первую строку flang --version.

Сохраните программу как скидка.flang:

модуль «Скидка»

тотальная функция «К оплате»
  принимает цена: неотрицательное, скидка: неотрицательное
  возвращает число
  обеспечивает «скидка не поднимает цену» результат не больше цена
  пример «скидка меньше цены»
    дано цена равно 1000
    дано скидка равно 150
    ожидается 850
  пример «скидка больше цены»
    дано цена равно 100
    дано скидка равно 150
    ожидается 0
  если скидка не меньше цена
    то 0
    иначе цена минус скидка

И проверьте:

$ flang check скидка.flang
модуль «Скидка»: функций 1, из них с доказанным завершением 1; типов 0
скидка.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ flang run скидка.flang --function "К оплате" --args '{"цена": 2500, "скидка": 400}'
не доказано: утверждений 1: доказано 0, сетка 1, на веру 0 — запуск только по явному согласию: --на-веру
…
$ flang run скидка.flang --function "К оплате" --args '{"цена": 2500, "скидка": 400}' --на-веру
на веру: доказанность не считалась — запуск по ключу --на-веру
2100

Это три разных ответа, и в них весь язык. check говорит: программа разобрана, типы сошлись, завершение доказано, оба примера прошли. run отказывается считать: постусловие «скидка не поднимает цену» подтверждено только двумя примерами, а не доказано для всех входов. С ключом --на-веру он считает, но пишет, что доказанность не проверялась. Почему ядро не доказало это неравенство и что с этим делать — в главе «Чего в языке пока нет».

Собрать компилятор из исходников можно на любой системе с компилятором C99 и make:

git clone https://github.com/digitable-lol/flang && cd flang
make -C bootstrap -j4
./bootstrap/flang check flang/stdlib/lists.flang

У такой сборки нет каталога share/flang: вне клона она не найдёт стандартную библиотеку и рантаймы целевых языков. У готовой сборки они есть.

Чем этот язык интересен, кроме обещания

Его можно прочитать целиком. Компилятор написан на самом flang и лежит в одном каталоге — flang/self/: лексер, парсер, система типов, анализ завершаемости, ядро доказательств и перевод во все десять языков. Около 131 тысячи строк (18 октября 2026, cat flang/self/*.flang flang/self/*/*.flang | wc -l). Достаточно большой, чтобы быть настоящей системой, и достаточно обозримый, чтобы прочитать за несколько вечеров.

Решения объяснены на месте. В исходниках и в docs/ подробно записано, что рассматривалось и почему отвергнуто.

Он собирает сам себя. В bootstrap/ лежат исходники на C, которые компилятор получил переводом самого себя. make -C bootstrap собирает из них двоичный flang, и этот flang умеет заново перевести flang/self/ в C. Как это устроено — глава «Компилятор на самом себе».

Чего в языке нет

Версия 0.x: синтаксис не заморожен, совместимость обещана только для формы JSON и кодов диагностик. Программы на flang вне репозитория языка есть, но пока их пишет та же команда, что и язык.

Из того, что заметно в первый день: порядка на строках (меньше только для чисел), замены элемента списка по номеру, изменяемого состояния, безымянных функций как значений, перехвата отказа. Ядро доказательств не доказывает законов над число (double) и законов монады. В готовой сборке нет программ перепроверки доказательств и английских сообщений — они работают из клона. Каждый пункт с программой и ответом компилятора — в главе «Чего в языке пока нет».

Маршрут трека

Начинать стоит с «Двух классов программ»: без этой главы остальные разваливаются на список конструкций.