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

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

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

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

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

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

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

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

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

Доказывается пятью способами, и каждый оставляет след в ведомости:

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

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

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

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

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

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

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

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

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

В flang их ноль, и список пуст проверяемо: стоит отдельный тест, тихо добавить нельзя.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Ноль. И это оказалось самым полезным результатом дня: замер показал, что узкое место не там, где все думали. Причина у 13 случаев из 15 была одна — принципа индукции не было ни у одного встроенного типа: ни у списка, ни у строки, ни у числа.

После того, как это починили, стало 7 из 20.

Замер повторяется, и он линейка: по ней видно, движемся ли мы к цели или просто наращиваем возможности. Условие, ради которого всё:

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

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

Дальше

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