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

У двоичного нет целых проверок, а не только более слабая ведомость, — и его собственная справка об этом молчит

Про разрыв между двумя реализациями уже записано, что ведомость двоичного бывает слабее ведомости на Node и никогда не сильнее (vedomost-dvoichnogo-byvaet-slabee-i-nikogda-ne-silnee). Это верно, но описывает не весь разрыв и описывает более мягкую его половину.

Вторая половина: целой проверки в двоичном может не быть вовсе. Тогда он не даёт слабый вердикт — он даёт зелёный вердикт и код возврата 0 на программе, которую вторая реализация отвергает.

Категорная поверхность в bootstrap/compiler_flang.c не реализована:

grep -c FUNCTOR bootstrap/compiler_flang.c
0

Замер на трёх порчах примера examples/cat/modules/, тех самых, про которые в шапке файла написано «каждая ломает сборку»:

порчасвидетель на Nodeдвоичный
в «Платёж по заказу» возвращён равным 0 вместо возвращён равным заказ.отменёнFLANG_FUNCTOR_SQUARE, код 1«замечаний нет», код 0
в категорию «Заказы» добавлена стрелка, функторы её не отображаютFLANG_FUNCTOR_NOT_TOTAL ×2, код 1«замечаний нет», код 0
в «Уценить платёж» минус 100 вместо минус 10000FLANG_FUNCTOR_SQUARE, код 1FLANG_EXAMPLE, код 1

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

Почему это хуже слабой ведомости. Слабая ведомость честна: она печатает "сила": null там, где не справилась, и правило сверки «слабее можно, сильнее нельзя» её ловит. Отсутствующая проверка не печатает ничего и потому неотличима от пройденной.

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

Правило, которое из этого следует. Перечень «чего нет у двоичного» не выписывать в справке руками, а считать: список видов проверок обязан читаться у обеих сторон и сравниваться между собой, как это уже сделано для перечня команд (cli-help-diverges-between-the-two-implementations). Выписанный руками список отстаёт от кода тем же молчанием — только здесь молчание стоит зелёного вердикта на сломанной программе.

Ещё три расхождения, найденные тем же прогоном (все на коммите cb3b7a18):

Чем подтверждено. Ветка vypusk/kurs, коммит cb3b7a18 (= github/main на 20 августа 2026). Двоичный собран из bootstrap/ этого же дерева (make -C bootstrap -j4, flang --versionflang 0.5.0), свидетель — node flang/bin/flang.mjs. Каждая строка таблицы снята отдельным прогоном с записью кода возврата.

Чем ограничено. Про категорную поверхность и три названных места командной строки. Полного списка «какие ещё виды проверок есть у свидетеля и нет у двоичного» этот замер не даёт — его и надо считать, а не выписывать.

Поправка от 20 августа 2026. Здесь стояло, что двоичный отвечает «замечаний нет» и кодом 0 на программе с категорной поверхностью. Это больше не так, и исправлено оно не сторожем, а самим двоичным. Он отвечает кодом 2 и называет пробел вслух:

$ bootstrap/flang check examples/cat/modules/payments.flang; echo $?
проверено НЕ ВСЁ: в программе объявлено то, чего бинарник не судит вовсе —
categories, morphisms. … Ответ «замечаний нет» здесь читался бы как
«проверено», а это неправда.
2

Замер по всему корпусу подделок: 13 подделок, 12 отвергнуты кодом 2 с названной поверхностью. Осталась ровно одна глухая — flang/test/fixtures/binary-rules/scale-mismatch.flang, уточнённые числовые типы (сотых, вес): они стоят типом в подписи, а не отдельной строкой, и отличить такую программу от обычной по объявлениям нечем. Она проходит кодом 0, и это сегодня правда, а не описка.

Прогон: node flang/scripts/binary-rules-guard.mjs на ветке svod-rask, коммит 66245238. Сам сторож при этом переписан: сравнивать состав правил двух реализаций больше не с чем — реализация на JavaScript удалена, — и вопрос «примет ли молча» спрашивается теперь прогоном подделок, а не чтением текстов.

Дополнение: правила не потеряны — они не подключены, и это меняет размер работы. Здесь и в соседних заметках разрыв читается как «проверок нет и писать их заново». Замер говорит другое: правила поверхности переписаны на самом flang и лежат в дереве — flang/self/monoid.flang (822 строки), monad.flang (620), iso.flang (334), functor.flang (751), sets.flang (1026), setoid.flang (1727), svoystva.flang (386), grid.flang (443) и четыре спрашивающих слоя law-oracle, functor-oracle, setoid-oracle, sets-oracle (1786 суммарно). Двенадцать файлов, 7 895 строк.

Ни один не входит в сборку двоичного. Замыкание по слову использует от flang/self/bootstrap/compiler.flang29 файлов, и этих двенадцати среди них нет; между собой они подключаются (setoid зовёт functor и monoid, monad зовёт sets), то есть образуют собственный остров рядом с компилятором.

Значит вопрос «почему двоичный не судит поверхность» — не про ненаписанное правило, а про строку использует, которой нет. Но одной строкой не кончится: семь из двенадцати слоёв сами не проходят flang checkmonad, sets, grid, law-oracle, functor-oracle, setoid-oracle, sets-oracle дают код 1; проходят monoid, iso, functor, setoid, svoystva.

Чем подтверждено. Обход использует от compiler.flang прогоном, ветка u/spec-cat от github/main (702a3602). Размеры — wc -l.

Связано: a-path-in-backticks-is-checked-against-nothing, vedomost-dvoichnogo-byvaet-slabee-i-nikogda-ne-silnee, cli-help-diverges-between-the-two-implementations, checks-that-stopped-comparing, the-installed-path-was-never-walked-end-to-end