flang — язык с доказуемым завершением Кодогенерация: одна программа на десяти языках
0%

Кодогенерация: одна программа на десяти языках

Кодогенерация: одна программа на десяти языках

Команда flang emit превращает программу на flang в программу на другом языке: с рантаймом, прогонщиком и файлом сборки. Всё в этой главе снято на flang 0.7.29 (готовая сборка для Linux x86_64) 18 октября 2026 года; целевые компиляторы — те, что стояли на машине: gcc и g++ 15.2.0, Go 1.26.5, rustc 1.97.1, javac 26, Elixir 1.20.3 на OTP 29, Node 26.7.0, Python 3.14.4, .NET 10.0.110.

Десять целей

Список целей бинарник называет сам — достаточно попросить несуществующую:

$ flang emit проба.flang --target zzz
flang emit: цели «zzz» у этой сборки flang нет — целей здесь ДЕСЯТЬ — «c», «cpp», «go», «rust», «java», «js», «ts», «elixir», «python», «csharp».

Код возврата 2 — неверный вызов. Node для вывода кода не нужен: все десять генераторов собраны в сам бинарник. Написаны они на flang — flang/self/emit-c.flang, emit-go.flang и ещё восемь файлов, около 35 тысяч строк вместе, — а в flang/src/emit/<цель>/ лежат готовые куски рантайма, которые копируются в вывод как есть.

Выводится только проверенное

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

тотальная функция «Длина числа»
  принимает х: число
  возвращает число
  длина х
$ flang emit ошибка.flang --target c --out out-c
FLANG_BUILTIN_ARGS в файле ошибка.flang, строка 6, столбец 9: «длина» принимает строку или список, а получила число
flang emit: печать отменена — программа не проходит проверку, замечаний 1.

Код 1, каталог out-c не создан. Коды emit: 0 — выведено и проверено всё, 1 — программа не прошла проверку, 2 — неверный вызов, 3 — выведено, но проверено не всё (так бывает с частями языка, которые эта сборка не проверяет до конца, — бинарник называет их поимённо).

Примеры внутри функций emit не запускает и прямо пишет об этом в выводе: «ПРИМЕРЫ НЕ ПРОГНАНЫ … Прогоните их отдельно: flang test <файл>». Поэтому рабочий порядок — flang check, flang test, потом flang emit.

Доказанное постусловие в код не попадает: проверять его при каждом вызове незачем. Недоказанное едет в код проверкой. Вот функция, у которой постусловие доказывается:

модуль «Обещание»

тотальная функция «Следующее»
  принимает х: число
  возвращает число
  обеспечивает «на единицу больше» результат равен (х плюс 1)
  пример «Два»
    дано х равно 2
    ожидается 3
  х плюс 1
$ flang emit обещание.flang --target go --out post-go
проверок при работе снято 1: постусловие доказано ядром обо всех входах и
проверено примерами функции — в напечатанный код оно не едет.
напечатано файлов 5, байт 119152, в post-go
…
$ grep -c "на единицу больше" post-go/flang/*.go
0

Если заменить тело на х умножить на 2, а постусловие — на «результат равен (х плюс х)», ядро его не доказывает (check --proof пишет «сетка 1 значение … это не доказательство»), и в выведенном Go появляется проверка rt.Post(…), которая на нарушении вернёт FLANG_PROPERTY.

Одна программа — десять сборок

Возьмём программу из двух функций над строками. Она проверяет заодно, что строки меряются кодовыми точками, а не байтами или единицами UTF-16:

модуль «Проба»

тотальная функция «Взять символ»
  принимает текст: строка, номер: число
  возвращает строка
  пример «Второй символ»
    дано текст равно "мир"
    дано номер равно 2
    ожидается "и"
  символ номер в текст

тотальная функция «Длина текста»
  принимает текст: строка
  возвращает число
  пример «Эмодзи считается одним»
    дано текст равно "мир 🌍"
    ожидается 5
  длина текст
$ flang check проба.flang
модуль «Проба»: функций 2, из них с доказанным завершением 2; типов 0
проба.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ flang test проба.flang
проба.flang: примеров 2, прошло 2, не прошло 0

Выводим во все десять целей:

$ for t in c cpp csharp elixir go java js python rust ts; do
    flang emit проба.flang --target $t --out out-$t
  done

Каждый запуск отчитывается строкой «напечатано файлов N, байт M»:

Цель Файлов Байт Что лежит в каталоге
c 6 557 869 proba.c, proba.h, рантайм, прогонщик, Makefile
cpp 7 575 181 то же на C++20
csharp 9 177 164 шесть классов, Proba.cs, flang.csproj, Makefile
elixir 4 145 367 proba.ex, рантайм, прогонщик, Makefile
go 5 120 372 go.mod, пакеты flang/, flangrt/, cli/, Makefile
java 8 157 025 шесть классов, Proba.java, Makefile
js 3 43 300 proba.js, flang_cli.js, package.json
python 4 102 674 proba.py, рантайм, прогонщик, Makefile
rust 7 173 413 Cargo.toml, src/*.rs, Makefile
ts 5 44 598 proba.ts, tsconfig.json, прогонщик, package.json

Почти весь объём — рантайм, одинаковый для любой программы. В C сама программа занимает 5 КБ (proba.c), а рантайм — около 450 КБ: представление значений, арена, UTF-8, счётчики шагов и глубины.

Собираем. Флаги сборки строгие и записаны в выведенных Makefile: код обязан собираться без единого предупреждения.

$ cd out-c && make
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto   -c -o flang_runtime.o flang_runtime.c
…
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto -o flang_cli flang_cli.o flang_runtime.o proba.o -lm -lpthread

У остальных целей так же: C++ — g++ -std=c++20 -Wall -Wextra -Werror -pedantic, Java — javac -encoding UTF-8 -Xlint:all -Werror, Elixir — elixirc --warnings-as-errors, Rust — cargo build, Go — go build, C# — dotnet build. Все семь собрались без замечаний.

Прогонщик: строка JSON на входе, строка JSON на выходе

У каждой цели рядом с программой выводится прогонщик с одним и тем же протоколом. Значения в нём размечены: {"n":"5"} — число (строкой, чтобы не потерять NaN, Infinity и -0), {"s":"…"} — строка, {"l":[…]} — список, {"v":"Имя","f":[…]} — вариант.

$ printf '%s\n' '{"fn":"Длина текста","args":[{"s":"мир 🌍"}]}' \
                '{"fn":"Взять символ","args":[{"s":"мир"},{"n":"2"}]}' | ./flang_cli
{"ok":true,"value":{"n":"5"}}
{"ok":true,"value":{"s":"и"}}

Тот же запрос всем десяти:

c      {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}
cpp    {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}
go     {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}
rust   {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}
java   {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}
js     {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}
ts     {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}
python {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}
elixir {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}
csharp {"ok":true,"value":{"n":"5"}} {"ok":true,"value":{"s":"и"}}

Команды запуска выведенный код подсказывает сам, в последней строке emit:

$ ./out-c/flang_cli
$ ./out-rust/target/debug/flang_cli
$ java -cp out-java FlangCli Proba
$ node out-js/flang_cli.js ./proba.js
$ node out-ts/flang_cli.js ./proba.ts
$ python3 out-python/flang_cli.py proba
$ elixir -pa out-elixir/_build -e 'Flang.Cli.main(["Proba"])'
$ dotnet out-csharp/bin/Debug/net8.0/flang.dll Proba

(каждую — из каталога своей цели). Про TypeScript оговорка: компилятора tsc на машине не было, поэтому проверки типов TypeScript не было; файл proba.ts запущен Node 26, который исполняет TypeScript, отбрасывая типы.

Модуль, а не только прогонщик

Прогонщик нужен для сверки; в обычной программе выведенный код подключают как модуль. JavaScript-модуль не имеет зависимостей и работает в Node и в браузере:

$ node -e 'import("./out-js/proba.js").then(m => {
    console.log(Object.keys(m).join(", "))
    console.log(m.dlinaTeksta("мир 🌍"), m.vzyatSimvol("мир", 2))
  })'
$PROGRAM, dlinaTeksta, vzyatSimvol
5 и

Имена функций переведены в латиницу по правилам цели: «Длина текста» стала dlinaTeksta в JavaScript, fn_dlina_teksta в Python, proba_dlina_teksta в C. Имя файла и класса берётся из имени модуля: proba.py, Proba.java.

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

Число flang — IEEE-754 double. В Java, C#, JavaScript, Go, Rust и C это родной тип, но не везде он ведёт себя одинаково: в Python 1.0 / 0.0 бросает ZeroDivisionError, а на BEAM (Elixir) значений NaN и бесконечности нет вовсе. Поэтому арифметика идёт через функции рантайма, а не через операторы цели, и рантайм выравнивает поведение. Проверим на трёх вызовах:

модуль «Арифметика»

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

тотальная функция «Частное»
  принимает а: число, б: число
  возвращает число
  а делить на б

Запросы: 0.1 + 0.2 = 0.3, 1 / 0, 0 / 0. Ответы восьми целей:

c      {"ok":true,"value":false} {"ok":true,"value":{"n":"Infinity"}} {"ok":true,"value":{"n":"NaN"}}
go     {"ok":true,"value":false} {"ok":true,"value":{"n":"Infinity"}} {"ok":true,"value":{"n":"NaN"}}
rust   {"ok":true,"value":false} {"ok":true,"value":{"n":"Infinity"}} {"ok":true,"value":{"n":"NaN"}}
java   {"ok":true,"value":false} {"ok":true,"value":{"n":"Infinity"}} {"ok":true,"value":{"n":"NaN"}}
js     {"ok":true,"value":false} {"ok":true,"value":{"n":"Infinity"}} {"ok":true,"value":{"n":"NaN"}}
python {"ok":true,"value":false} {"ok":true,"value":{"n":"Infinity"}} {"ok":true,"value":{"n":"NaN"}}
elixir {"ok":true,"value":false} {"ok":true,"value":{"n":"Infinity"}} {"ok":true,"value":{"n":"NaN"}}
csharp {"ok":true,"value":false} {"ok":true,"value":{"n":"Infinity"}} {"ok":true,"value":{"n":"NaN"}}

Вычислитель flang отвечает так же: flang run арифметика.flang --function "Частное" --args '{"а":1,"б":0}' последней строкой печатает Infinity.

Как каждая цель этого добивается, объяснено в шапках её рантайма:

  • Python — деление ловит ZeroDivisionError и возвращает бесконечность или NaN (flang_runtime.py); число в текст переводит свой number_text, потому что repr(1.0) даёт «1.0», а flang печатает «1».
  • Elixir — число хранится как {:num, float() | :nan | :inf | :ninf}: конечные значения — обычные float, остальные — атомы.
  • Go — свой NumberText вместо strconv.FormatFloat, у которого другие пороги перехода к экспоненте.
  • C# — double, а не decimal: decimal десятичный, без NaN и бесконечностей, и 0.1 + 0.2 дало бы ровно 0.3 (шапка Value.cs).

Отсюда и общее устройство значения во всех целях: один размеченный тип «тег плюс данные» вместо родных типов цели. Rust умеет суммы типов сам, Java — запечатанные интерфейсы, но выведенному коду нужно структурное равенство любых двух значений, доступ к полю по имени и приём значения снаружи через JSON — проще и надёжнее одно представление на всё.

Функции-значения

Функцию в flang можно передать аргументом. Пять из десяти целей замыканий в нужном виде не имеют, поэтому перед выводом кода функции-значения снимаются одним проходом (flang/self/defunc.flang): значение-функция становится вариантом с тегом, применение — вызовом функции-распределителя. Генераторам целей приходит программа без функций-значений.

модуль «Высший порядок»

тотальная функция «Удвоить»
  принимает х: число
  возвращает число
  х умножить на 2

тотальная функция «Прибавить»
  принимает слагаемое: число, х: число
  возвращает число
  слагаемое плюс х

тотальная функция «Применить дважды»
  принимает действие: функция из числа в число, х: число
  возвращает число
  действие от (действие от х)

тотальная функция «Пятёрка удвоена дважды»
  возвращает число
  пример «пять, десять, двадцать»
    ожидается 20
  «Применить дважды» от функция «Удвоить» и 5

тотальная функция «Десятка прибавлена дважды»
  возвращает число
  пример «пять, пятнадцать, двадцать пять»
    ожидается 25
  «Применить дважды» от (функция «Прибавить» с слагаемое равным 10) и 5

В выведенном C распределитель выглядит так:

fl_status vysshiy_poryadok_primenit_1(fl_ctx *ctx, fl_value teg, fl_value a1,
                                      fl_value *result, fl_error *error) {
  if (fl_variant_is(teg, "Удвоить")) {
    return vysshiy_poryadok_udvoit(ctx, a1, result, error);
  } else if (fl_variant_is(teg, "Прибавить с слагаемое")) {
    fl_value slagaemoe = fl_nothing();
    FL_TRY(fl_variant_field(ctx, teg, "слагаемое", &slagaemoe, error));
    return vysshiy_poryadok_pribavit(ctx, slagaemoe, a1, result, error);
  } else {
    return fl_match_fail(ctx, teg, error);
  }
}

Частично применённая функция «Прибавить» с слагаемое равным 10 стала вариантом с полем слагаемое — захваченное значение едет полем варианта. Функцию можно передать и снаружи, тегом:

$ printf '%s\n' '{"fn":"Пятёрка удвоена дважды","args":[]}' \
                '{"fn":"Десятка прибавлена дважды","args":[]}' \
                '{"fn":"Применить дважды","args":[{"v":"Удвоить","f":[]},{"n":"5"}]}' | ./flang_cli
{"ok":true,"value":{"n":"20"}}
{"ok":true,"value":{"n":"25"}}
{"ok":true,"value":{"n":"20"}}

Программа, которая не останавливается

Обычная (не тотальная) функция может не завершиться. flang её не запрещает, но вычислитель считает шаги:

модуль «Зацикливание»

функция «Вечность»
  принимает н: число
  возвращает число
  «Вечность» от (н плюс 1)
$ flang check вечность.flang
модуль «Зацикливание»: функций 1, из них с доказанным завершением 0; типов 0
без доказанного завершения: «Вечность»
вечность.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ flang run вечность.flang --function Вечность --args '{"н":0}'
…
FLANG_RECURSION_LIMIT: функция «Вечность» исчерпала лимит шагов (40000000) на глубине вызовов 1

Выведенный код тоже считает шаги — во всех десяти целях. Предел по умолчанию в выведенном коде — миллион шагов (#define FL_MAX_STEPS 1000000 в C, ctx.max_steps = … в Python), ответ один и тот же:

$ echo '{"fn":"Вечность","args":[{"n":"0"}]}' | ./flang_cli
{"ok":false,"code":"FLANG_RECURSION_LIMIT","message":"функция «Вечность» исчерпала лимит шагов (1000000) на глубине вызовов 1"}

Эту строку дословно вернули сборки Go, Rust, Java, JavaScript, TypeScript, Python, Elixir и C#. Предел задаётся ключом --max-steps:

$ flang emit вечность.flang --target python --out v42 --max-steps 4242
$ echo '{"fn":"Вечность","args":[{"n":"0"}]}' | python3 v42/flang_cli.py zaciklivanie
{"ok":false,"code":"FLANG_RECURSION_LIMIT","message":"функция «Вечность» исчерпала лимит шагов (4242) на глубине вызовов 1"}

Не путать с --step-limit: тот ограничивает шаги самого бинарника flang на этот запуск, а --max-steps впечатывается в выведенный код.

Известная поломка 0.7.29: C и C++ эту программу не собирают. Хвостовой самовызов разворачивается в for (;;) без выхода, параметр result остаётся неиспользованным, и строгие флаги из выведенного Makefile превращают предупреждение в ошибку:

$ cd v-c && make
cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -flto   -c -o zaciklivanie.o zaciklivanie.c
zaciklivanie.c: In function ‘zaciklivanie_vechnost_body’:
zaciklivanie.c:15:55: error: unused parameter ‘result’ [-Werror=unused-parameter]
cc1: all warnings being treated as errors

То же у C++ (g++ -std=c++20 … -Werror). Обход — собрать без -Werror: make CFLAGS='-std=c99 -O2' для C и make CXXFLAGS='-std=c++20 -O2' для C++; так собранные программы отвечают той же строкой про миллион шагов. Касается это только функций, которые никогда не возвращают значение; программы, которые завершаются, собираются со строгими флагами.

Предел глубины вызовов тоже сохраняется во всех целях. В C, C++, Rust, Python, Java и C# вычисление ради этого идёт в отдельном потоке с большим стеком (pthread_attr_setstacksize в C, thread::Builder::stack_size в Rust, threading.stack_size в Python): переполнение стека там не диагностика, а падение процесса, и предел языка должен сработать раньше.

Процессы: C, JavaScript и Elixir

У flang есть процессы с почтовыми ящиками и надзор (глава «Синтаксис по факту»). Выводить их умеют не все цели. Возьмём счётчик из репозитория, docs/examples/reference/ru/counter.flang: процесс «Счётчик», надзор «Учёт» и прогон «два прибавления».

$ flang emit counter.flang --target python --out p-python
flang emit: печать отказала — у цели «python» нет планировщика конкурентности, а в программе объявлена конкурентность (процессов 1, надзоров 1, прогонов 1), первый — процесс «Счётчик». … Цели с планировщиком: c, elixir, js

Код 1. Так же отказывают cpp, go, rust, java и csharp; c, js, ts и elixir программу выводят. Прогон запускается запросом {"run":"…"}:

$ cd p-elixir && make build
$ echo '{"run":"два прибавления"}' | elixir -pa _build -e 'Flang.Cli.main(["Counter"])'
{"ok":true,"run":"два прибавления","исход":"покой","пробегов":2,"состояния":[["Счётчик",{"r":[["всего",{"n":"5"}]]}]],"живые":["Счётчик"],"журнал":["Счётчик","Счётчик"],"отказы":[]}

Выведенный C отвечает тем же итогом (состояние счётчика — 5), только с полным журналом доставок. У JavaScript процессы выводятся, но прогонщик запрос run не понимает: {"ok":false,"code":"CLI","message":"неизвестное поле запроса"}.

На Elixir отображение почти дословное — оно записано в шапке выведенного flang_conc.ex:

flang Elixir/OTP
процесс GenServer
состояние процесса состояние GenServer
обработчик чистая функция flang, вызываемая из handle_info
почтовый ящик почтовый ящик процесса BEAM
отправить send
отложить send самому себе — в конец очереди
продолжить {:noreply, …, {:continue, …}}
через … отправить Process.send_after
надзор супервизоры OTP

Два места не совпали. Стратегия в flang задаётся каждому дочернему процессу отдельно, а «передать отказ выше» в OTP — свойство супервизора, а не ребёнка. Поэтому один надзор flang выводится тремя супервизорами OTP с разной интенсивностью перезапусков. И второе: в flang перезапуск сохраняет почтовый ящик, а на BEAM ящик умирает с процессом. Выведенный код в terminate/2 сохраняет непрочитанные сообщения, а новое воплощение процесса забирает их в init/1. Между смертью процесса и регистрацией нового имени есть короткое окно: сообщение, отправленное именно в него, пропадёт — это записано в той же шапке.

Мелочи, о которых заботится генератор

  • Порядок вычисления — строго слева направо. Каждое выражение, которое может дать ошибку, выводится отдельным оператором, чтобы первой сообщалась левая ошибка, как у вычислителя flang. В Elixir порядок вычисления аргументов не гарантирован, поэтому каждый аргумент становится отдельной привязкой.
  • Сообщения об ошибках копируются дословно, вместе с кавычками-ёлочками: код и текст ошибки — часть поведения программы.
  • Управляющие символы двунаправленного текста (U+202E и подобные, на которых строится атака Trojan Source, CVE-2021-42574) в строковых литералах всегда экранируются. Проба со строкой "а‮б⁦в" на 0.7.29: ни в одной из десяти целей сырого символа нет; в C и C++ он записан восьмеричными байтами ("а\342\200\256б\342\201\246в"), в Rust и Elixir — \u{202e}, в остальных — ‮. Значение строки при этом то же — Java, Elixir и C# вернули его байт в байт.

Чем проверяется перевод

Один пример с десятью одинаковыми ответами — не доказательство, что перевод верен. В репозитории для этого три механизма.

Сверка целей между собой в CI. Работа emit-guard (.github/workflows/ci.yml, план scripts/targets/emit-and-examples.fscript) выводит программы в девять целей — все, кроме ts, — собирает их, запускает и сравнивает ответы с C. Чтобы сверка не была пустой, CI нарочно портит рантайм Go (умножение заменяется сложением) и требует, чтобы расхождение нашлось.

Протокол перевода для C. Ключ --protocol кладёт рядом с C-кодом протокол: какой узел исходника каким правилом из закрытого списка (flang/translation/PRINT-RULES.tsv) стал какими строками C. Отдельная программа на C99, flang/translation/matcher.c, flang не разбирает и ничего не переводит — она сличает протокол с текстом:

$ flang emit проба.flang --target c --out pr-c --protocol pr.txt
$ cc -O2 -o matcher flang/translation/matcher.c
$ ./matcher проба.flang pr-c/proba.c pr.txt
узлов в протоколе 14; переиграно правилом 7, принято на слово 0
СОШЛОСЬ

Стоит поменять в proba.c одно имя — и ответ НЕ СОШЛОСЬ с номером строки.

Сверка C с формальной семантикой языка по функциям. Для каждой функции выведенного C подбираются входы из её типов (для признаков и простых вариантов — вся область), и ответ C сравнивается с ответом семантики языка, записанной на Lean (docs/translation-validation.ru.md, запуск — run-script translation:validate).

Чему из этого нельзя доверять слепо, репозиторий перечисляет сам в docs/trust-gaps.ru.md: рантайм C держится примерами и пробами, компилятору C доверяют без проверки, а девять целей кроме C доказательной проверкой перевода не покрыты — только сверкой ответов.

Что унести из главы

  • Выводится только программа, прошедшая проверку; примеры — отдельно, flang test.
  • Одна программа даёт десять сборок с одинаковыми ответами, включая крайние случаи double, Unicode и предел шагов.
  • Функции-значения снимаются до генераторов, поэтому у каждой цели логики для них нет.
  • Процессы есть только в C, JavaScript/TypeScript и Elixir, и прогон процессов запускается в C и Elixir.
  • Обычная функция, которая никогда не возвращается, в 0.7.29 не собирается строгими флагами C и C++.

Дальше — глава «Компилятор, написанный на самом себе»: вывод в C — это путь, которым flang собирает сам себя без Node.

Нашли неточность? Выделите фрагмент текста — рядом появится жучок.

Нужен разбор именно вашей ситуации?

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

Доска запросов
Дальше