flang

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

Язык вырос из FTS (Formal Type Surface) — языка исполняемых спецификаций для описания предметных областей. Сегодня это две поверхности одного проекта, и путать их не стоит.

Справка двоичного обещает, что .fts он не берёт: «Мост из FTS („.fts“-модели, законы поверх них) бинарник не принимает вовсе» (flang check --help). На прогоне выходит хуже отказа. flang check разбирает модель как программу без функций и печатает зелёное с кодом 0 — ровно то же, что на пустом файле. flang check --proof договаривает: «нет объявленных функций», «нет объявленных законов», а теорема — «объявлено, не доказано: старая форма (наследие FTS)». Зелёный ответ на .fts проверки не значит, и опираться на него нельзя.

Канал поставки FTS закрыт решением владельца 31 августа 2026 года. Пакет @digitable-lol/fts при этом не исчез: версия 0.4.7 стоит в зависимостях портала, и из неё собрана вендорная копия, на которой работает песочница раздела. Язык ставится формулой — brew install digitable-lol/tap/flang, двоичный 0.7.3.

Предметную область сегодня записывают на самом flang: это fspec, и о нём отдельный раздел ниже.

Особенности

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Дальше нужна оговорка, без которой весь раздел читается неверно: правил категорной поверхности двоичный компилятор сегодня не судит вовсе. Он разбирает объявления, проверяет типы, завершаемость, доказательства и примеры, а дойдя до законов поверхности, называет непроверенное поимённо и выходит кодом 2 — «проверено НЕ ДО КОНЦА», потому что «замечаний нет» здесь читалось бы как «проверено». Судья не потерян, он не подключён: слои, считающие эти законы, написаны на самом flang (flang/self/monoid.flang, monad.flang, iso.flang, functor.flang), но в сборку двоичного не входят, а прежняя реализация на JavaScript, которая их считала, снята. Всё, что ниже сказано словом «проверяется», — это контракт flang/cat/SPEC.md, а не сегодняшний ответ команды.

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

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

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

Монада объявляется на параметрическом типе и называет две функции — возврат и соединение. Отображение эндофунктора при этом не объявляется вовсе: у полиномиального функтора оно ровно одно, и компилятор выводит его из устройства типа. На том же стоит форма в монаде — do-нотация словами, которая разворачивается внутри разбора в обычные вызовы, поэтому все девять целей получают её даром (flang/cat/MONAD.md).

Естественные преобразования по-прежнему только описаны в контракте flang/cat/SPEC.md и не реализованы, но причина сместилась: раньше мешал сам параметрический полиморфизм, теперь он есть — мешает то, что связь морфизмов знает имя типа, а не применение (flang/cat/POLY.md, фаза 3).

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

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

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

Диагностика выдаётся в JSON с кодом, уровнем и местом, поэтому пригодна для машинного разбора — это существенно для сценария, где код пишет не человек. Но код с приставкой FTS_ — свойство прежней поверхности, и поставленный двоичный 0.7.3 таких кодов не печатает вовсе: в исходниках компилятора (flang/self/) коды диагностик — с приставкой FLANG_, ни одного с приставкой FTS_. Три примера выше показывает песочница этой страницы; инструмента, который выдал бы их на вашей машине, сегодня нет.

Реализация

Реализация одна: компилятор flang написан на flang — 118 918 строк в 60 файлах flang/self/**. Он печатает сам себя и ещё в девять целевых языков.

Реализация-свидетель на TypeScript и JavaScript, служившая определением поведения языка, снята 20 августа 2026 года: 48 файлов, 56 072 строки. Разницу это меняет не только в счёте файлов. Всё, что считала она и чего перенос на flang ещё не догнал, сегодня не считается никем — и дерево называет это прямо, а не молчит: пробы, написанные против свидетеля, лежат в flang/test/ и не запускаются, потому что обрываются на ввозе снятого файла.

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

Круг раскрутки замыкается семенем: в дереве лежит тот же компилятор, заранее напечатанный в C99. Из семени одним make собирается двоичный, тот печатает исходники заново, из печати собирается второй двоичный — и второй обязан совпасть с первым байт в байт. Сверяет это sh scripts/raskrutka.sh --check по семи файлам, а расхождение называет файлом, байтом и строкой, а не словом «не совпало». Семя перепечатывают руками, и пока оно не догнало исходники, круг разомкнут: проверка отказывает и говорит, на чём.

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

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

brew install digitable-lol/tap/flang

Формула кладёт один двоичный flang, библиотеку с заголовками, исходники рантайма C в share/flang/c и страницу руководства man flang. Из внешнего ей нужен только make; Node.js не нужен ни при установке, ни в работе. Такой способ распространения применяли и другие самоприменяющиеся языки: Go долго возил сгенерированный C, Nim возит до сих пор. Проблема начальной загрузки остаётся у тех, кто развивает сам язык.

Второй путь — собрать из исходников; он же нужен тому, кто правит сам язык:

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

На выходе bootstrap/flang — тот же инструмент, что кладёт формула. Node в сборке не участвует.

Что поставилось, спрашивают у самого двоичного: flang --version и flang -v отвечают flang 0.7.3, flang --help и flang -h перечисляют команды, man flang описывает их подробно.

Проверка живёт прямо в этом бинарнике: flang check файл.flang проходит разбор, связывание, типы, завершаемость, доказательства и примеры и печатает замечания словами — с кодом и местом. На сошедшемся файле в ответе стоит слово «проверено»; файл с ошибкой типов уводит двоичный кодом 1 и называет код беды — FLANG_TYPE. Ведомость доказательства печатает flang check --proof: машине — --json, в файл — --записать.

Команд у него двенадцать — check, test, run, emit, ast, tokens, facts, io, lock, package, repl и lsp. Считает двоичный тоже сам: flang run файл.flang --function «Имя» вычисляет функцию без Node и без cc. Печатает — во все девять целей: flang emit файл.flang --target c и так же go, rust, java, js, elixir, python, csharp; каталог из --out заводится сам.

Служба для ИИ-помощника лежит в том же двоичном, но подана не подкомандой, а ключом: flang --mcp-mode — JSON-RPC по стандартным потокам, по сообщению на строку, и запускает её помощник, а не человек. Средств у неё два: flang_check проверяет программу целиком и вместе с ведомостью, flang_prove отвечает, чем доказано одно названное обещание. Поля «ок» в ответах нет намеренно: три вердикта уходят порознь — «доказано» обо всех входах, «сетка N» на значениях автора и «объявлено, не доказано». Как прописать службу помощнику, печатает flang --mcp-mode --help.

Одну оговорку про печать надо знать заранее, иначе она встретится на первой же команде. Рантайм цели уезжает в вывод дословно, то есть читается с диска — ищется в --runtime, затем в $FLANG_RUNTIME_DIR, затем рядом с поставленным двоичным, в share/flang/<цель>. Формула кладёт один рантайм из восьми — share/flang/c, и в архиве релиза лежит только он. Значит из brew-установки сразу работает печать в C, а для остальных семи целей --runtime придётся указать на дерево исходников (flang/src/emit/<цель>).

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

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

Ограничения

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

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

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

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

Пользовательские свойства проверяются, а не доказываются. Доказываются завершение, типы и то, что принимает ядро доказательств: аксиом у него ноль, каждый шаг обязан назвать факт, а ядро только сверяет — искать оно не умеет и не должно. Пользовательские свойства и примеры проверяются на конечной сетке входов. Ведомость об этом печатает flang check --proof, и слова в ней не взаимозаменяемы: «доказано» стоит только у утверждений про все входы, а у сетки написано «нарушений не найдено», потому что «не нашли» и «нет» — разные утверждения; а там, где прогона примеров не было, стоит «нарушений НЕ ИСКАЛИ», и это третье, не сводимое к первым двум. Законы категорной поверхности сегодня не считает никто: слои есть, но к двоичному не подключены. Документация обязана различать эти случаи: «проверено на N входах» — не то же самое, что «доказано».

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

Эффекты выражаются описанием, а не выполняются. Язык чистый; работа с сетью или файлами — это построение описания действия, которое исполняет хозяин, среда, в которую напечатан модуль. Поручения объявлены самим языком одной закрытой суммой «Поручение» — не автором программы, потому что поручение есть контракт между языком и хозяином; набор покрывает файлы и октеты в них, каталоги, запуск процессов, соединения, запрос по сети, время и случайное число. Рядом — объявление план и команда flang io с четырьмя кодами выхода: 0 — дошли, 1 — программа сдалась сама, 2 — кривой вызов, 3 — сломался инструмент. Хозяин здесь свой, а не на Node, и границы у него названы отказом, а не молчанием: экрана нет (FLANG_IO_NO_SCREEN), своей криптографии нет ни байта, а https исполняет внешний curl — нет его, и в ответе FLANG_IO_NO_TLS. Функции, строящие поручения, проверяются обычными примерами и остаются тотальными — сеть в язык не входит. Монады ввода-вывода при этом нет, и вместо неё машина продолжений (flang/cat/SPEC.md, «Чем это не монада»). А вот слой исполнения для НАПЕЧАТАННОЙ программы сделан для одной цели из восьми — Node.

fspec: доказанное правило и то, что не даёт его отменить

Механизм зовётся fspec, и держится он на одном: спека — не markdown, а программа на самом языке. Правило предметной области записывается рядом с функцией, и компилятор доказывает его для всех входов, а не для тех, что придут в бою:

модуль «Спека 1: потолок скидки»

тотальная функция «Потолок скидки»
  принимает сумма: число
  возвращает число
  обеспечивает «скидка не больше 30» результат не больше 30
  пример «потолок»
    дано сумма равно 1000
    ожидается 30
  30

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

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

make -C bootstrap -j8                  # собрать компилятор, если его ещё нет
bootstrap/flang io fspec/guard.flang   # или короче: ./ярлык spec:check

Ответ — одна строка с числами:

спеки согласны: спек 42, утверждений 295, и каждое доказано из нуля аксиом; обещаний в слепке 100, и у каждого цель та же; видов перевода 2, и каждый обещает то же, что основной

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

См. также

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

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

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

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

• fspec/README.md — спеки на flang и проверка их согласия

• docs/guide/project-layout.ru.md — раскладка репозитория и куда что кладут

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

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

• Словарь языка — все формы со всеми написаниями и все конструкции подряд, для вычитки целиком

• Практикум — восемь ступеней, вердикт по заданию выносит исполнение

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

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

• Библиотеки на языке — flang-tui и flang-env: что на flang уже написано целиком, без второго языка в дереве