Цена доказательства измерена: 0 из 20, и тесты нашли четыре ошибки против нуля

Первый замер того числа, от которого зависит судьба проекта — condition-for-the-revolution. Ответ оказался жёстче любого прогноза.

Отбор воспроизводимый и не подыгрывающий: все 185 функций flang/stdlib, порядок «файл, объявление», взята каждая девятая. Не «которые понравились».

Исходы: ядро закрыло само — 0; теорема принята — 0; не вышло — 20, из них «ядро не берёт» 15, «на языке не выразить» 5.

Как читать этот ноль. Он не значит, что доказательства бесполезны — он значит, что сегодня доказать обычную функцию библиотеки нельзя вообще, и разговор про «дешевле или дороже тестов» пока преждевременен. Дороже стало бесконечно: за 9 минут работы получено ноль.

Тесты за то же время дали четыре настоящие ошибки. Это честный результат не в нашу пользу, и он записан именно так.

Чем ограничено. Замер сделан на origin/main, до вливания веток с новыми правилами ядра. Повторить на своде — обязательно, число должно сдвинуться.

Улики не пересказаны, а сохранены: 20 файлов работы в docs/benchmark/ с настоящими текстами отказов. Ветка work/zamer-tseny, отчёт docs/benchmark-proof-cost.md, 479 строк (было 475: 19 августа в отчёт вписана поправка о том, что слово требует в языке появилось, — сам замер она не трогает).

Замер повторён 16 августа: стало 2 из 20. Те же двадцать функций, основание origin/main = 17d6853. Ноль не устоял, а вместе с ним не устояла и фраза «доказать обычную функцию нельзя вообще»: два утверждения закрылись, и оба — без теоремы, одной строкой постусловия. Что при этом НЕ изменилось: теорем написано 14, принято ядром по-прежнему 0; тесты нашли те же четыре ошибки, ни одна не починена; новых ошибок не нашла ни одна из двух работ. Разбор — в bottleneck-moved-to-body-shape и в docs/benchmark-proof-cost-2.md.

Связано: no-induction-for-builtin-types, condition-for-the-revolution, unstatable-costs-more-than-unprovable, a-measured-zero-is-valuable, bottleneck-moved-to-body-shape