flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Четыре поверхности записи

Одну программу flang можно записать четырьмя наборами слов: русским, английским, эсперанто и китайским. Это не четыре языка и не перевод. если, if, se и 如果 — одно и то же слово языка, записанное четырьмя способами, и разбор даёт одно дерево.

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

Писать можно на четырёх. Доказывать — на двух

русскаяанглийскаяэсперантокитайская
обычная программадададада
печать в чужой языкдададада\*
доказательство и завершаемостьдаданетнет

\* Строка про печать появилась 29 августа 2026, и до того дня она была бы неверна: китайская программа не печаталась НИ ВО ЧТО, а эсперантская печаталась с потерянными буквами. Разбор ниже — «Печать молчала тоже». Починено в исходниках печати; в собранном компиляторе появится после перепечатки семени, и на четырёх целях из восьми — python, java, csharp, elixir.

Второй строкой всё и сказано. Язык продаёт доказуемость; словаря доказательств на эсперанто и китайском нет, и написать требует, обеспечивает, убывает или индукция по на них не на чем. Программа на китайском проверится и запустится; доказать о ней что-нибудь вы не сможете.

Поэтому дерево и написано на двух поверхностях из четырёх, а не на четырёх: эсперанто и китайский существуют в таблице целиком, но пользоваться ими всерьёз пока нельзя — из 1101 программы дерева на них написаны две, обе демонстрационные, и лежат они в examples/surfaces/.

Полная таблица слов — на странице Словарь языка; она печатается из той же единственной таблицы, по которой разбирается любой файл, и пустая клетка в ней значит, что слова нет.

Что именно молчит

Десять понятий на двух поверхностях — это всё доказательства

Самое важное здесь не число, а то, ЧТО именно молчит. Все десять понятий, открытых только на русской и английской поверхностях, — словарь доказательств и завершаемости:

Понятиерусскаяанглийскаяэсперантокитайская
requiresтребуетrequires
ensuresобеспечиваетensures
claimутверждаемclaim
forallдля всехfor all
inductionиндукция поinduction on
byPropertyпо свойствуby property
byExampleпо примеруby example
byHypothesisпо предположениюby hypothesis
qedследовательно доказаноtherefore proved
decreasesубываетdecreases

Причина названа в самой таблице: у этих понятий нет устоявшегося слова ни в эсперанто, ни в китайском, а requires и ensures стоят парой в Eiffel, JML и Dafny. Придуманное слово хуже отсутствующего: сказать, что китайское доказательство пишется наполовину по-английски, — значит соврать дважды.

Печать молчала тоже, и это было хуже словаря

Словарь молчит громко: пустая клетка в таблице видна. Печать молчала тихо, и узнать об этом можно было, только попробовав.

$ flang emit examples/surfaces/factorial.zh.flang --target python
flang emit: печать отказала — имя функции «乘积» даёт идентификатор «fn_value»,
уже занятый (функции «前置») — переименуйте одно из имён в модели

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

Имя в исходникеБылоСтало
«乘积»value乘积
«前置»value前置
«阶乘»value阶乘
«De unu ĝis kvin»de_unu_is_kvinde_unu_ĝis_kvin
«Antaŭmeti»anta_metiantaŭmeti

Беды при этом две разные. У китайского словарных символов не остаётся ВОВСЕ, поэтому все имена схлопывались в одно слово value — и печать честно отказывала по столкновению, вместо того чтобы напечатать четыре разные функции под одним именем. У эсперанто буква просто выпадала: ĝis («до») становилось is, имя печаталось и молча меняло смысл.

Цель эти буквы принимает — это проверено прогоном, а не вычитано из стандарта. Одна и та же функция fn_乘积 собрана и запущена на всех четырёх целях, у которых своя транслитерация, и все четыре ответили 24:

python  24     java    24     csharp  24     elixir  24

Отказ остался там, где имя действительно не выводится. Знаки препинания по-прежнему разделители, имя из одного препинания по-прежнему даёт value, а столкновение имён по-прежнему отказ, а не молчаливое переименование.

Четыре цели из восьми — c, go, js, rust — пока печатают по-старому: go, js и rust ввозят разбиение имени у цели c, а цель c заморожена до конца перепечатки семени. Отдельно замерено, что дело не в самом языке C: fn_乘积 собирается и работает и там — cc -std=c99 -Wall -Wextra -Werror -pedantic не сказал ни слова. Значит там это не «нельзя», а «пока нельзя трогать».

Шесть понятий на трёх поверхностях

ПонятиерусскаяМолчитПочему
moduleмодульэсперантоmodulo в эсперанто значит и модуль, и остаток от деления, а остаток таблица уже отдала resto de. Одно слово не вправе означать две конструкции
notнеэсперантологическое «не» в эсперанто ne, но ne таблица уже отдала литералу лжи. Файл на эсперанто пишет отрицание функцией «Не так» из stdlib/logic.flang
opPercentпроцентовкитайскаякитайский процент — приставка (百分之十), а не слово после числа
nestedвложен объектэсперанто
embeddingвложениеэсперанто
supervisionнадзорэсперанто

Одно понятие на одной поверхности

alias — русское это («список чисел» это …). Английского, эсперантского и китайского слова у него нет вовсе: это единственное понятие таблицы, доступное только на русской поверхности.

Счёт целиком

Открыто наПонятийДоля
всех четырёх поверхностях13388,7 %
трёх64,1 %
двух106,8 %
одной10,7 %
всего в таблице150

По поверхностям: русская — 150 понятий из 150, английская — 149, китайская — 138, эсперанто — 134. Всего фраз в таблице 633: у понятия слов бывает несколько (равен, равна, равно).

Одна строка, четыре записи

если н не больше 1     то 1  иначе н умножить на («Факториал» от (н минус 1))
if n is at most 1      then 1  else n times («Factorial» of (n minus 1))
se n ne pli granda ol 1  tiam 1  alie n fojoj («Faktorialo» de (n minus 1))
如果 n 不大于 1          那么 1  否则 n 乘以 («阶乘» 的 (n 减 1))

Это четыре строки из четырёх файлов дерева, а не выдумка страницы: examples/rosetta/factorial.flang, examples/rosetta/factorial-english.flang, examples/surfaces/factorial.eo.flang, examples/surfaces/factorial.zh.flang. Каждый проходит проверку сам по себе — одной и той же командой, меняется только имя файла:

flang check examples/rosetta/factorial.flang
flang check examples/surfaces/factorial.zh.flang

Все четыре отвечают одинаково: «функций 5, из них с доказанным завершением 3; типов 0» и «замечаний нет».

Имена МОДУЛЕЙ у всех четырёх с 29 августа 2026 английские — «Factorial», «Factorial», «Faktorialo», «Factorial zh», — и это правило Р7 (имена в коде): имя модуля становится именем напечатанного файла, а от кириллического имени он выходил транслитом, от иероглифического — пустым словом value; ни то, ни другое не читается. Поверхность выбирается ключевыми словами и именами функций, а не именем модуля: в русском файле по-прежнему «Факториал» от (н минус 1).

Насколько «одно дерево» — правда

Утверждение «разбор даёт одно дерево» стоит проверить, а не принять на слово, — и в сыром виде оно неверно.

Сырые деревья не совпадают. У каждой из трёх поверхностей с русским образцом расходятся 76 слотов:

Что разошлосьСлотов
name — имена функций, параметров, примеров, типов46
ключи args в примерах — имена параметров11
локальные имена (н/n, начало/start, конец/finish, первое/element, элементы/items)14
acc, item — связки свёртки4
module — имя модуля1

Все 76 — имена, которые выбрал автор: «Факториал», «Factorial», «Faktorialo», «阶乘». Имя — не язык. Ни один из 76 слотов не разбор: ни kind, ни op, ни данные задачи. 2432902008176640000 во всех четырёх файлах написано одинаково — двадцать факториал не переводится.

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

sha256 ccd7ae71250e3dd1425f3fbdb8a028252e37f85dbd39e3eb5de6247f2c4850ab
       — один и тот же у всех четырёх

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

Как это устроено

Таблица одна: понятие → слова на четырёх поверхностях. Она лежит в разборе языка одной константой SURFACE_TABLE, и из неё печатается всё остальное — плоский список слов, словарь диагностик, страница Словарь языка и числа этой страницы. Второго списка нет, поэтому разъехаться нечему.

Поверхность файла определяется большинством голосов среди ключевых слов, а не первым словом: файл на эсперанто начинается с английского module, потому что эсперантского слова у этого понятия нет, и по первому слову вся диагностика файла говорила бы по-английски.

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

Перепроверить

./ярлык поверхности:прогон    перемерить
./ярлык поверхности:проверка  сверить числа этой страницы с прогоном

Этот сторож не стоит в CI, и знать об этом важнее, чем читать числа выше. Сборка сайта (node docs/site/build.mjs --check) о поверхностях не знает и остаётся зелёной, когда страница врёт; звать поверхности:проверка приходится руками. Ровно так страница и пролежала с тремя устаревшими размерами файлов, пока их отсюда не убрали совсем: размер файла мерил длину комментария в шапке, а не язык.