flang

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

Язык вырос из FTS (Formal Type Surface) — языка исполняемых спецификаций для описания предметных областей. FTS остаётся тотальным подмножеством flang: любая модель .fts является валидной программой языка и вычисляется одинаково обеими реализациями.

Особенности

Два класса программ

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

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

Разделение имеет прямое следствие: во встраиваемом режиме проверки фактов допускаются только тотальные функции. Система, отвечающая на вопрос «подтверждено или нет», не имеет права зависнуть.

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

Печать в целевые языки

Программа печатается в исходный код на восьми языках: C, Go, Rust, Python, Java, C#, Elixir и JavaScript.

Печать сопровождается дифференциальной сверкой: напечатанный код обязан давать те же значения, те же коды и те же тексты ошибок, что интерпретатор. Для каждой цели это проверяется на 31 программе, 154 функциях и 2235 точках сетки входов, а сетка строится не только из примеров, но и из порчи каждого аргумента заведомо чужими значениями — иначе диагностики остались бы непроверенными.

Такая сверка находит дефекты, невидимые для тестов отдельно взятого бэкенда. За время разработки так были найдены: печать некомпилируемого C при совпадении имени варианта и функции; литерал варианта, превращавшийся в запись в бэкенде Go; знаковый ноль при делении на бесконечность в Elixir.

Словесный синтаксис

В синтаксисе используются только слова: из … в …, после, цепочка … сначала … затем …, сохраняет композицию. Русская и английская поверхности равноправны и компилируются в одно синтаксическое дерево.

Категорная поверхность

Морфизм объявляет стрелку между объектами категории; композиция записывается словом после, а длинная цепочка — в порядке чтения:

морфизм «отгрузить» из «Заказ» в «Отгрузка»
морфизм «выставить» из «Отгрузка» в «Счёт»
морфизм «оформить» это «выставить» после «отгрузить»

цепочка «провести заказ»
  сначала «отгрузить»
  затем «выставить»
  затем «оплатить»

Стыковка композиции проверяется компилятором и относится к доказанному: «б» после «а» собирается тогда и только тогда, когда кодомен «а» равен домену «б». Несостыковка называет, что с чем не сошлось:

FLANG_COMPOSE_MISMATCH: «выставить» приводит в «Счёт», а «отгрузить» ожидает «Заказ»

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

Моноид объявляется носителем, операцией и единицей; с обращением он становится группой — отдельного слова нет, потому что группа и есть моноид с обращением. Здесь граница «доказано / проверено» проходит внутри одной конструкции: доказывается устройство (операция — функция двух аргументов носителя, единица — значение носителя), а сами законы — ассоциативность, нейтральность, обратимость — проверяются на конечной сетке из примеров операции. Доказать их нельзя: это равенства вычислений на всех значениях носителя.

Изоморфизм и бифунктор объявляются и проверяются тем же сличением объявлений. У изоморфизма при этом само равенство «обратный после прямого = единица» не проверяется вовсе — ни доказательством, ни на сетке: у стрелки категории нет тела, вычислять нечего. Это допущение автора, и компилятор отвечает лишь на то, осмысленно ли оно сформулировано.

Естественные преобразования и монады описаны в контракте flang/cat/SPEC.md и не реализованы: монада требует эндофунктора, а он невыразим без параметрического полиморфизма, у которого сделана только первая фаза.

Разбор суждений

Помимо ошибок синтаксиса и типов проверка сообщает о дефектах в самих правилах: недостижимых свойствах, дырах в покрытии входа и перекрытии правил. Анализ интервальный и точный для условий, сравнивающих поле с константой; условия, связывающие поля между собой, честно помечаются непроанализированными.

FTS_COVERAGE_HOLE          при «сумма» ∈ (−∞, 10000) не срабатывает ни одно
                           правило — результат остаётся начальным (0)
FTS_PROPERTY_VIOLATED      свойство «Скидка ограничена» нарушается при
                           «сумма» ∈ (−∞, 0): результат 0 против предела −200000
FTS_PROPERTY_UNATTAINABLE  предел «результат ≤ 20 % от поля «сумма»» не берётся
                           нигде, где правила меняют результат

Диагностика выдаётся в JSON с кодом, уровнем и местом, поэтому пригодна для машинного разбора — это существенно для сценария, где код пишет не человек.

Реализации

Существуют две реализации, и обе поддерживаются намеренно.

Эталонная написана на TypeScript и JavaScript. Служит определением поведения языка.

Самоприменяющаяся написана на самом flang: лексер (84 функции), парсер (374), проверка типов (277), анализ завершаемости (124), печать в C (326) и связывание модулей. Ядро FTS переписано отдельно — 300 функций, все тотальные, с побайтовым совпадением вывода с эталоном на каждой модели репозитория.

Лексер самоприменения тотален целиком — 84 функции из 84, — и это стоит отметить, потому что раньше их было 54 из 88. Разница ровно в одном: посимвольный проход перестал ходить по позиции. Убывала разность «размер минус позиция», то есть число; теперь строка раскладывается в список, и рекурсия по хвосту доказывается.

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

Эталонная реализация не удаляется: относительно неё и проверяется схождение.

Установка и переносимость

Релиз содержит компилятор, уже напечатанный в C99, поэтому установка требует только компилятора C:

brew install digitable-lol/tap/flang

Node.js для установки не нужен. Такой способ распространения применяли и другие самоприменяющиеся языки: Go долго возил сгенерированный C, Nim возит до сих пор. Проблема начальной загрузки остаётся у тех, кто развивает сам язык.

Проверка живёт прямо в этом бинарнике: flang check файл.flang проходит разбор, связывание, типы и завершаемость и печатает замечания словами — с кодом и местом. Команды перечисляет flang --help, подробно описывает man flang.

Оболочка flang repl есть и здесь: вычислителя в бинарнике нет, поэтому она печатает сессию в C, собирает её системным cc против поставленного рядом рантайма и запускает; без cc она продолжает проверять разбор, типы и завершаемость.

Полный инструментарий — восемь бэкендов, интерпретатор и сервер MCP — распространяется через npm и требует Node:

npm install -g @digitable-lol/fts

Рантайм не содержит архитектурно-зависимых конструкций; выравнивание вычисляется объединением базовых типов, то есть берётся максимальное для платформы. Компилятор собран кросс-компилятором под RISC-V и запущен под эмуляцией без единой правки исходного кода: значения совпали с x86-64 до последнего знака, включая 0.1 плюс 0.2 = 0.30000000000000004, NaN и Infinity.

Ограничения

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

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

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

Параметрический полиморфизм работает и в репозитории. Параметры типа объявляются у типов и у функций, применяются, выводятся при вызове, и печать их не стоит ничего — все восемь целей типы и так стирают. Долгое время пользоваться этим было нельзя: парсер самоприменения полиморфизма не понимал, а корпус сверки собирается по маске каталога, поэтому первый же такой файл в библиотеке ронял неподвижную точку. Теперь понимает — и монада выразима: тип «Возможно» от «А», функция «Обернуть» от «А», связывание с параметром типа функция из «А» в («Возможно» от «Б») проходят разбор, типы и завершаемость. Осталась одна фаза: свести optional.flang и result.flang в параметрические, то есть переписать уже написанное.

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

Расширение доказуемого возможно: условия, укладывающиеся в линейную арифметику, разрешимы, и подключение решателя к условиям верификации остаётся открытой задачей.

Эффекты выражаются описанием, а не выполняются. Язык чистый; работа с сетью или файлами — это построение описания действия, которое исполняет хозяин, среда, в которую напечатан модуль. Сделано: пять поручений (чтение и запись файла, запрос по сети, время, случайное число), объявление план, хозяин на Node и команда flang io. Функции, строящие поручения, проверяются обычными примерами и остаются тотальными — сеть в язык не входит. Монады ввода-вывода при этом нет: она требует параметрического полиморфизма, и вместо неё — машина продолжений (flang/cat/SPEC.md, «Чем это не монада»). Слой исполнения написан для одной цели из восьми.

См. также

• flang/SPEC.md — спецификация языка

• flang/core/SPEC.md — контракт ядра FTS, написанного на flang

• flang/self/SPEC.md — контракт самоприменения и его долги

• flang/cat/SPEC.md — контракт категорной поверхности

• docs/language.ru.md — справочник синтаксиса FTS

• Страница языка — песочница, быстрый старт и решения задач

• Справочник конструкций — 45 карточек на все формы языка

• Курс по FTS — предметная область как исполняемая спецификация

• Курс по flang — устройство компилятора изнутри