Подпись не определяет функцию: на нашей библиотеке она однозначна в 36,5 % случаев

Вторая половина замысла владельца сильнее первой и заслуживает честного счёта. Вопрос заменяется: не «дай код с хешем X» (это разобрано в code-cannot-be-derived-from-its-hash и не работает), а «дай функцию, удовлетворяющую этой спецификации». Тогда работает вывод, а не перебор, и flang для этого устроен лучше многих: ядро с нулём аксиом (zero-axioms) проверит любого кандидата и не ошибётся.

Ядро действительно не ошибётся. Ошибётся спецификация.

Замер. Взял все 208 объявлений flang/stdlib/, у которых есть подпись (то есть строка принимает; функции без аргументов сюда не попали), стёр имена параметров и оставил подпись — типы входов по порядку и тип выхода. Различных подписей вышло 114. Из них ровно одну функцию называют 76:

подпись однозначна в 36,5 % случаев. В 63,5 % она называет класс, а не функцию.

Самые населённые классы:

В классе строка → строка лежат «В верхний регистр», «В нижний регистр», «Обрезать пробелы», «Обратить строку», «Первый символ», «Заглавная буква» и ещё шесть. Синтезатор, которому сказали строка → строка, вправе отдать любую из двенадцати, и ядро подтвердит: спрошено ровно это. Это тот самый разрыв, о котором proven-is-not-correct, только с числом.

Постусловия помогли бы, но их не пишут. обеспечивает стоит у 7 функций из 208 — 3,4 %. Добавление постусловия к подписи поднимает однозначность с 36,5 % до 38,9 %: плюс два процентных пункта. Примеры тоже не спасают — их 484 на 208 функций, 2,3 на функцию, а две-три пары «дано–ожидается» не определяют функцию ни в каком смысле.

И честное число в пользу замысла, потому что оно есть. Спецификация короче тела: 692 строки против 2461, отношение 0,28 — тело длиннее спеки в 3,6 раза, и так у всех 208 функций без исключения. То есть если бы синтез работал, хранить пришлось бы в 3,6 раза меньше. Не «ничего» — в 3,6 раза меньше.

Но экономить нечего. Весь исходник flang/stdlib/ — 378 537 байт (370 КиБ); весь код на flang в репозитории — 3,4 МиБ; кодовая база Unison со стандартной библиотекой — 16,7 МиБ (unison-measured). Замысел «не хранить пакеты» бережёт единицы мегабайт, платя за это машино-часами вывода. Место — не дефицитный ресурс, это уже было измерено, и вывод там тот же: вопрос закрыт, это не проблема.

Что из этого следует по существу. Чтобы спецификация определяла функцию, её надо дописать до объёма, при котором она перестанет быть короче тела, — и тогда вы пишете программу дважды. Это не наблюдение про flang, это общее место синтеза: спецификация, достаточно точная, чтобы задать программу, есть программа. Наш замер даёт этому месту число: сегодня спека составляет 28 % от тела, а однозначна в 36,5 % случаев.

Чем подтверждено. Замер на /srv/flang-rabota/packages, ветка work/packages-research, 2026-08-18, по 13 файлам flang/stdlib/. Подпись собирается из строк принимает и возвращает (по одной на функцию: grep -h '^\s*принимает' flang/stdlib/*.flang | wc -l = 208, столько же возвращает), имена параметров отбрасываются, типы сохраняются по порядку. Строки спецификации — принимает, возвращает, обеспечивает, убывает, требует и блоки пример целиком; строки тела — всё остальное внутри объявления, кроме комментариев и пустых строк.

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

• Число про нашу систему типов, а не про синтез вообще. У flang типы грубые: нет уточняющих типов, поэтому строка → строка и не может различать двенадцать функций. У Liquid Haskell или Synquid подпись говорит гораздо больше — но ровно на столько, на сколько удлиняется сама подпись, и это уже видно в отношении 0,28.
• Однозначность мерена по классам подписи, а не по тому, найдёт ли синтезатор нужное. Хороший синтезатор с примерами сузит класс из двенадцати; насколько — здесь не мерено.
• Дубли в замере настоящие, а не ошибка счёта. В классе список числа → число «Сумма», «Произведение», «Минимум», «Максимум» встречаются дважды: они объявлены в двух модулях. Это находка про библиотеку, а не про метод.
• Про горизонт синтеза замер не говорит ничего. Он говорит только, что цель синтеза сегодня задана неточно.
• Библиотека уехала от прозы. docs/modulnost-i-pakety.md пишет «12 файлов, 4301 строка, 185 функций» по состоянию на 2026-08-15; на 2026-08-18 в flang/stdlib/ 17 файлов и 8218 строк, а объявлений с подписью — 208 (сторож чисел: не про сегодняшнее дерево — оба числа названы датой). Это ровно тот случай, о котором a-number-without-a-named-measure: число в прозе без названного измерителя не перепроверяется. Здесь измеритель назван.

Связано: code-cannot-be-derived-from-its-hash, proven-is-not-correct, zero-axioms, unstatable-costs-more-than-unprovable, unison-measured, zakony-kak-ukazatel