Два правила языка живут только в реализации на JavaScript, и сверка двух реализаций их не видит

Компилятор существует дважды: реализация на JavaScript и компилятор, написанный на самом flang. Их согласие проверяется прогоном одних и тех же программ через обе стороны и сравнением ответов. Проверка зелёная — и всё же два правила языка есть только на одной стороне.

Первое. Функция без строки возвращает: реализация на JavaScript отвергает её кодом FLANG_TYPE, компилятор на flang принимает молча — подставляет джокер вместо типа результата.

Второе. Тотальная функция, зовущая обычную из постусловия: реализация на JavaScript отвергает кодом FLANG_NOT_TOTAL, компилятор на flang молчит. Слово postconditions в flang/self/totality.flang не встречается ни разу.

Почему сравнение двух реализаций молчит

Оно сравнивает ответы на программах, которые есть в дереве. Ни одна программа дерева так не написана: у всех есть возвращает, и ни одна тотальная не зовёт обычную из постусловия. Правило, на которое не наступает ни одна программа, для такого сравнения невидимо — оно проверяет не правила, а поведение на имеющемся материале.

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

Чем подтверждено. Изъятием, а не чтением: правило про возвращает снято из flang/src/types.mjs — красным стал ровно один тест во всём дереве. Прогонялись types, self-types, corpus-claims, stdlib-claims, claim-guard, spec-guard, результат сверен с полным прогоном дерева.

Связано: a-rule-no-corpus-program-touches-is-invisible-to-the-reference-check, flang-test-is-always-green-on-a-layer-with-no-examples-of-its-own, the-binary-is-silent-about-checks-it-does-not-have