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

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

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

Из этого обещания растёт всё остальное в языке, и именно оно объясняет, зачем ещё один язык, когда их и так много.

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

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

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

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

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

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

обеспечивает — постусловие. Строка после него утверждает, что́ верно про результат. Компилятор проверяет это утверждение, а не верит на слово. Здесь: результат должен совпасть со встроенной длиной списка — то есть функция обязана сойтись со вторым, независимым способом посчитать то же самое.

пример — тест внутри функции. Три примера здесь — не документация: их выполняет flang test, и они лежат вплотную к коду, а не в отдельном файле, который забудут обновить.

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

Писать можно не только по-русски. Поверхностей у языка четыре — русская, английская, эсперанто и китайская, — все равноправны, и компилятор строит из них одно и то же дерево разбора; как устроен этот механизм и как добавить свою, разбирает глава «Своя поверхность». Вот подлинный файл 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

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

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

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

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

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

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

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

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

flang решает это так: действие в нём описывается, а не выполняется. Функция возвращает поручение — «прочитать такой файл», «запросить такой адрес», — и остаётся чистой; исполняет поручение отдельная команда flang io, снаружи. Граница между «что решено» и «что сделано» проходит по типу значения, а не по дисциплине программиста.

Это тот же приём, ради которого в других языках заводят монады эффектов, только без монад: план действий — обычное значение, его можно напечатать, сравнить, проверить и только потом исполнить.

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

Написанное на flang правило не обязано оставаться в flang. Команда emit печатает программу в один из девяти целевых языков:

flang emit скидка.flang --target go --file skidka.go

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

Отсюда типичный сценарий: правило пишут и доказывают на flang, а работает в продакшене напечатанный Go или C — без рантайма языка в зависимостях.

Двенадцать команд

У двоичного файла flang двенадцать команд; вот те, что нужны в первый день:

Коды возврата одни у всех команд: 0 — чисто, 1 — не прошло, 2 — неверный вызов, 3 — сделано, но проверено не всё, и непроверенное названо поимённо. Полный справочник — в главе «Инструмент».

У файла программы четыре равноправных расширения: .flang, .fp, .фп и .фланг. Команды принимают любое.

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

brew install digitable-lol/tap/flang
flang --version        # 0.7.3

Или из клона — нужен только компилятор C, ни Node, ни Python:

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

Обе дороги дают один и тот же двоичный файл, собранный из C99.

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

Его можно прочитать целиком. Компилятор flang написан на самом flang и лежит в одном каталоге — flang/self/: лексер, парсер, система типов, анализ тотальности, ядро доказательств и печать во все девять целей. Около 130 тысяч строк на срез от 3 сентября 2026 года. Это редкий размер: достаточно большой, чтобы быть настоящей системой, достаточно обозримый, чтобы прочитать за несколько вечеров.

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

Он собирает сам себя. Компилятор пересобирается из собственных исходников через C-семя в bootstrap/. С одной честной оговоркой: семя перепечатывают вручную, а не на каждое изменение, поэтому проверка «семя соответствует сегодняшним исходникам» временами красная. На работу компилятора это не влияет — просто семя не сегодняшнее до следующей перепечатки.

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

Версия 0.x, и обещаний на будущее язык не раздаёт: совместимой поверхностью объявлены только канонический JSON и коды диагностик, синтаксис растёт через документированные предложения.

Внешних пользователей за пределами репозитория пока нет. Гарантии стабильного синтаксиса — тоже. Отдельная глава, «Чего в языке пока нет», держит список недостач поимённо — и она гниёт быстрее любой другой страницы этого трека, поэтому сверена с датой.

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

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