Файл, записанный на четырёх поверхностях, доказательство нести не может

У языка четыре равноправные поверхности — русская, английская, эсперанто, китайская. Восемь слов слоя доказательств есть только на двух из них. Значит любой файл, служащий образцом всех четырёх, доказательство нести не может в принципе, а не по недосмотру.

Наткнуться на это легко и обидно: правка выглядит как одна строка обеспечивает, а роняет проверку, которая про эту строку ничего не знает.

Чем подтверждено. 18 августа в examples/rosetta/factorial.flang была добавлена одна строка постусловия и теорема на восемь строк. Ядро их приняло — доказано индукцией по «нат», — и английский двойник тоже. Красным стало третье место:

$ node --test flang/test/surfaces.test.mjs
✖ ключи [flang,functions,legacy,module,theorems,types]
       ≠ [flang,functions,legacy,module,types]

factorial.flang — единственный файл набора Rosetta, записанный на четырёх поверхностях (examples/surfaces/factorial.eo.flang, factorial.zh.flang), и сверка деревьев требует совпадения всех четырёх. У эсперанто и китайской поверхности узла theorems быть не может: слов для него в таблице flang/src/lexer.mjs нет — намеренно, а не забыли.

Правка была снята. Вместо неё доказательства ушли к трём другим задачам витрины (hundred-doors, palindrome, towers-of-hanoi), у которых поверхностей две.

Что при этом НЕ потеряно. Доказательство про факториал в дереве есть: flang/proof/examples/corpus-factorial.flang — побайтовая копия той же функции плюс две строки, и совпадение копии с оригиналом проверяет flang/test/proof-kernel.test.mjs. То есть утверждение доказано, просто живёт не на витрине.

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

Правило на будущее. Прежде чем ставить обеспечивает или теорема в файл примеров — проверить, не служит ли он образцом более чем двух поверхностей:

grep -rl "$(basename файл .flang)" flang/test/surfaces.test.mjs

Связано: a-hand-written-list-outlives-the-tree, bottleneck-moved-to-claim-shape, byte-for-byte-comparison