Доказательства: зачем и как

Это главное отличие языка, и оно требует объяснения — потому что слово «доказательство» в программировании обычно означает что-то другое.

Чем доказательство отличается от теста

Тест проверяет входы, до которых вы додумались. Доказательство отвечает про все входы сразу — включая те, о которых никто не подумал.

пример «Дважды два»            ← один вход
  дано н равно 2
  ожидается 4

обеспечивает результат равно (2 умножить на н)    ← все входы

Обе строки полезны, и обе остаются в языке. Разница в том, что примеры вы пишете вечно, а доказательство пишется один раз.

Что происходит с завершаемостью

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

Доказывается пятью способами, и каждый оставляет след в отчёте, который печатает flang check --proof:

Последние две строки честно отделены: там завершаемость не доказана до конца, и разницу подхватывает проверка во время работы программы. Отчёт показывает это отдельным числом — 145 место у 107 функций, — а не прячет в общий итог.

Числа в таблицах этой страницы печатал компилятор 23 августа 2026 и с тех пор не перепечатывал: семя точки раскрутки отстало от исходников на 44 файла, и среди них proof-kernel, proof, obligations, totality, types — те, что решают, что считать доказанным. Отчего так и чем меряется разрыв — на странице Что доказано, а что нет.

Три ответа, а не два

Ядро отвечает тремя разными способами, и смешивать их нельзя:

Доказано ядром — утверждение верно про все входы. Таких 407 из 1045.

На сетке — проверено на наборе значений, нарушений не нашлось. Строка отчёта про это заканчивается словами «Это не доказательство», и заканчивается так намеренно: перебор конечного набора ничего не доказывает.

Объявлено, не доказано — ядру не хватило правил. Утверждение при этом проверяется во время работы, на тех входах, которые придут.

Когда ядро не закрыло цель само, у автора есть тот же выход, что в Coq и Isabelle: написать доказательство руками. Слово теорема со структурными шагами (дано, утверждаем, затем … по свойству «…», индукция по …, следовательно доказано) — поверхность в духе Isar, и ядро проверяет такой вывод шаг за шагом, ничего не ища. В дереве языка таких теорем 182, из них 55 в стандартной библиотеке. Отличие от Coq и Lean не в наличии этой возможности, а в том, как часто до неё доходит: вердикт печатает отдельным числом, сколько утверждений закрыто без единой написанной строки доказательства.

Есть и четвёртый ответ, самый ценный: НАРУШЕНО — контрпример найден, и он показывается. Не «доказать не вышло», а «вот вход, на котором ваше утверждение ложно».

Ноль аксиом — что это значит

Аксиома — то, что принимается на веру, без доказательства. В Coq и Lean аксиомы есть, и ими пользуются: классическое исключённое третье, аксиома выбора. Каждая — то, что машина не проверяет.

В flang их ноль, и это не обещание, а прогон. Аксиому в ядро нельзя «положить»: списка аксиом там нет как устройства, её можно только написать словами. Поэтому отдельная программа читает исходник ядра доказательств целиком и требует, чтобы слова «аксиома» в нём не стояло нигде, кроме названных доводов, объясняющих, почему то или иное правило — теорема; сверка идёт в обе стороны, так что и довод без слова в ядре — беда. Она же сверяет список подделок с каталогом flang/test/fixtures, тоже в обе стороны.

flang io flang/scripts/kernel-forgeries.flang --plan 'Аксиом ноль'
→ аксиом ноль, нарушений 0; 36 файлов каталога — все под надзором   (код 0)

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

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

Чего ноль аксиом не даёт

Доверять всё равно приходится, просто меньшему: что двенадцать решающих правил написаны верно, что реализация ядра верна, что компилятор под ней верен, что железо считает правильно.

И это не теория. За одни сутки в самих правилах нашлось шесть дыр, где ядро печатало «доказано обо ВСЕХ входах» там, где прогон находит контрпример.

Все шесть закрыты, и теперь стоит проверка на весь класс: если отчёт сказал «обо всех входах» — перебор обязан не найти контрпример. Проверяется это на всех утверждениях, какие есть в репозитории, а не на тех, что вспомнили.

Как устроено ядро

Двенадцать решающих правил, и каждое можно прочесть целиком; ядро называет их по именам в текстах отказов, и счёт берётся у самого ядра (grep -c 'тотальная функция «Правило' flang/self/proof-kernel.flang → 12). Большинство спрашивает ФОРМУ цели («не меньше 0», «не больше литерала», «равно», «не больше терма», «содержит», «начинается», «не убывает»); остальные не спрашивают: «цель есть допущение» сличает цель с допущением знак в знак, «несовместимые допущения» закрывает недостижимый случай, «развёртка по конструктору» разворачивает определение. Плюс два хода сверх правил: замкнутое выражение — это значение, его надо посчитать, а не выводить, и разбор цели по условию если.

Правил было три, потом восемь, и старые разделы спецификации называют их так, как было на день написания. Сегодня их двенадцать, и спорить с этим числом можно только с ядром в руках.

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

Отсюда же и решение не брать внешний решатель судьёй. Довериться ему значит отдать корректность двумстам тысячам строк чужого кода. Как подсказчику — можно и полезно. Как источнику истины — нет.

Чего доказательство не говорит

Самое важное на этой странице, и обычно об этом молчат.

Доказательство говорит, что код соответствует спецификации. Оно ничего не говорит о том, выражает ли спецификация ваше намерение.

Если постусловие написано неверно — код будет корректно делать не то. Это единственная причина, по которой формальные методы за пятьдесят лет не захватили индустрию, и никакое ядро её не отменяет.

Сколько это стоит

От этого ответа зависит, нужен ли язык вообще, поэтому цена измерена, а не оценена.

Двадцать обычных функций библиотеки — каждая девятая из всех 1474, чтобы не выбирать удобные, — и на каждую написаны и тесты, и доказательство.

Читать эту таблицу надо так: доказательство дороже тестов и находит меньше.

Сколько из тех же двадцати функций ядро закрывает, считает отдельный прогон, и считает механически — подменой тела на заглушку, а не списком имён:

./ярлык доказательства:20

На сегодняшнем дереве он отвечает так: доказано хоть что-нибудь у 14 функций из 20, содержательно — у 10. По утверждениям: содержательных 11, ослабленных 6 (доказаны и при теле-заглушке, то есть верны про любую функцию такой подписи), даровое 1 (тело переписано в постусловие), не проверено 2.

Число это ходит вверх и вниз вместе с ядром, поэтому в прозе его не набирают руками — берут прогоном.

Замер — это линейка, и по ней видно, движется язык к цели или просто обрастает возможностями. Цель названа одной строкой:

Доказательство должно стоить дешевле, чем тесты, которые оно заменяет.

Сегодня в мире оно дороже в 5–20 раз — поэтому доказывают только ядра операционных систем, криптографию и авионику. Если цена упадёт ниже цены тестов, меняется не язык, а то, что делают программисты: доказательство пишется один раз и покрывает все входы, тесты пишутся вечно.

Дальше

• Ядро отказало: чья это ошибка — что делать с каждым отказом
• Спецификация ядра — правила целиком
• Что доказано, а что нет — граница проведена явно
• Замер цены доказательства — отчёт с числами
• База знаний — что измерено и что оказалось ложным