Вывод из спецификации работает там, где область сузили нарочно, — и у flang такая область уже есть: словарь между спеками

Отрицательный вывод про синтез (synthesis-from-a-spec-hits-75-tree-nodes) неполон без второй половины: есть три места, где «не хранить код, а выводить его» работает и стоит в проде. Общее у всех трёх одно, и это не лучший перебор.

Первое: арифметика в конечном поле. fiat-crypto (MIT) выводит корректную-по-построению модульную арифметику из короткой функциональной спецификации, покрывая 80 простых полей. Внедрение по их же словам: «today about half of HTTPS connections opened by Web browsers worldwide use our fast verified code», а две кривые, попавшие в BoringSSL, «together account for over 99 % of ECDH connections» (github). Что выводится: около ста строк линейного C на операцию. Ни ветвлений, ни рекурсии, ни структур данных. Цена: «between tens of seconds and levels best run overnight», а прочерки в их таблицах означают, что вывод не уложился в память или время.

Второе: двоичные форматы. Narcissus (ICFP 2019) выводит из объявительной спецификации формата сразу упаковщик и распаковщик плюс машинно проверенное доказательство, что они обратны друг другу. Размер спеки — «each format typically requires 10 to 20 lines of declarative serialization code and 10 to 20 lines of record-type, enumerated-type, and numeric-constant declarations» (arXiv). Из этого получен пакетный слой Ethernet, ARP, IPv4, TCP, UDP и имён DNS, вставленный в mirage-tcpip при 15–30 строках стыковки на формат, с накладными расходами меньше процента.

Третье: подстановки в строках. FlashFill (POPL 2011) — три строковых оператора, меньше 5000 строк на C#, среднее время меньше 0,1 с, до десяти примеров — и около миллиона вызовов в неделю в Excel.

Общее у трёх, и это главный вывод заметки:

Выигрыш взят сужением языка, а не улучшением поиска. Везде, где вывод из спецификации работает, кто-то заранее выкинул из области почти всё.

И вот отсюда — единственное конкретное предложение для flang. У нас уже объявлена такая узкая область, и она ровно той же формы, что у Narcissus:

функтор «Заказ в счёт» из «Продажи» в «Биллинг»
  объект Покупка отображается в «Счёт»
    поле сумма отображается в поле «сумма без НДС»

Это объявительное описание соответствия данных — то же самое, что у Narcissus описание формата. Сегодня компилятор по нему проверяет: словарь состоит из существующих слов (compat.mjs, 760 строк, the-dictionary-between-specs-was-mute) и квадрат перевода сходится с контрпримером — FLANG_FUNCTOR_SQUARE (module-links-need-a-named-data-translation). Чего он не делает — не выводит саму функцию перевода. А это ровно та задача, на которой вывод из спецификации показал себя в проде: узкая, замкнутая, без рекурсии и ветвлений, с готовой теоремой правильности (тот самый квадрат) и готовым проверяющим (ядро с нулём аксиом, zero-axioms).

То есть замысел владельца «выводить по теоркату, а не хранить» выполним ровно на одном участке: перевод данных между двумя спеками. Не библиотека, не модуль — перевод. Зато с уже написанной половиной работы.

Чем подтверждено. Разбор внешних источников 2026-08-18, ссылки построчно выше. Состояние словаря и квадрата в дереве — прогоны, описанные в the-dictionary-between-specs-was-mute и module-links-need-a-named-data-translation (9 из 9 и три снятые порчи соответственно).

Чем ограничено.

• Narcissus не кнопочный, и это сказано прямо: «we emphasize that DeriveDecoder is interactive: if it gets stuck on a goal it cannot solve with the current rule libraries, it presents that goal to the user to solve interactively». Новый формат — это новые правила вывода, написанные руками.
• Цены вывода для нашего случая нет. Что стоит вывести функцию перевода по словарю — не оценено ни строкой, ни часом. Это заявка на работу, а не план.
• Спрос не измерен. Функторов в дереве четыре, все в examples/ (zakony-kak-ukazatel). Выводить пока нечего.
• Квадрат — опровержение, а не доказательство. Он сходится на конечной сетке из примеров автора; выведенная функция была бы проверена, но не доказана — тот же предел, что и у всей категорной проверки.

Связано: synthesis-from-a-spec-hits-75-tree-nodes, a-ratchet-instead-of-derivation, module-links-need-a-named-data-translation, the-dictionary-between-specs-was-mute, zakony-kak-ukazatel, category-theory-transports-truth, a-signature-does-not-determine-a-function