Минимальное доказательство корректности программы

Почему программисты об этом не думают

Программист не рассуждает о коде с точки зрения минимального доказательства корректности не из лени и не из глупости. У него этого нет в картине мира. Его учили:

• «код работает, если тесты зелёные»;
• «пиши проще, рефактори позже»;
• «доказывать что-то — это для академиков»;
• «формальные методы — это Coq, это годы, это не для нас».

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

Задача — не заставить всех писать на Coq. Задача — встроить привычку минимального доказательства в ежедневную работу так, чтобы она стала такой же естественной, как git commit.

---

Что такое «минимальное доказательство корректности»

Это не формальная верификация. Это рассуждение, которое отвечает на три вопроса для каждого фрагмента кода:

1. Что этот код обещает? (контракт: предусловие → постусловие)

2. Почему он это выполняет? (инвариант, который сохраняется)

3. Что может это нарушить? (границы доверия, внешний мир, неполнота модели)

Минимальное доказательство — это цепочка утверждений, каждое из которых либо очевидно, либо сведено к предыдущему. Если цепочка рвётся — там баг. Не в коде — в рассуждении.

Пример:

def max_of_list(xs):
    return max(xs)

Минимальное доказательство:

• Обещание: вернуть максимальный элемент.
• Почему: max возвращает максимальный элемент.
• Что нарушает: пустой список → ValueError.

Один вопрос — и сразу видно дыру. Не «тесты не покрыли», а обещание не выполнено для пустого входа. Это и есть минимальное доказательство: 10 секунд рассуждения вместо часа отладки.

---

Почему это ловит 98% багов

Логические баги делятся на классы, и почти все ловятся минимальным доказательством:

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

---

Почему программисты этого не делают

1. Нет языка для этого

Программиста учили писать код, а не рассуждать о коде. У него нет слов для контрактов, инвариантов, границ доверия. Он говорит «функция делает X», а не «функция обязуется X при условии Y, и вот почему».

2. Нет привычки

Никто не требует доказательства на code review. Ревьюер смотрит «выглядит нормально», а не «докажи, что это работает».

3. Нет инструментов

Тесты — это наблюдение, а не доказательство. Типы — это частичное доказательство. Но между «тесты зелёные» и «доказано» — пропасть, которую нечем заполнить.

4. Культура «двигаться быстро»

«Докажи» звучит как «тормози». Хотя на самом деле минимальное доказательство ускоряет: 10 секунд рассуждения экономят часы отладки.

---

Как помочь: пять шагов

Шаг 1. Дать язык

Ввести в обиход минимальный словарь:

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

Эти слова должны звучать на code review так же естественно, как «рефакторинг» и «техдолг».

Шаг 2. Встроить в ритуалы

На code review — три вопроса к каждому PR:

1. Что этот код обещает?

2. Почему он это выполняет?

3. Что может это нарушить?

В commit message — контракт, а не «fix bug».

В тестах — не «проверить, что работает», а «опровергнуть гипотезу о нарушении».

Шаг 3. Сделать дешёвым

Минимальное доказательство должно занимать секунды, не часы. Для этого:

• типы вместо комментариев (компилятор проверяет контракт);
• assert вместо молчаливых предположений;
• Unknown-ветки на границах доверия;
• инварианты в структурах данных (зависимые суммы, а не наборы флагов).

Шаг 4. Показать выгоду

Не «докажи, что ты не дурак», а «вот баг, который ты бы поймал за 10 секунд рассуждения». Каждый пойманный баг — это история успеха минимального доказательства.

Шаг 5. Встроить в обучение

Учить не «как писать код», а «как рассуждать о коде». С первых дней:

• вот контракт;
• вот инвариант;
• вот граница доверия;
• вот почему это работает;
• вот что это нарушает.

Не как отдельный курс по формальным методам, а как ежедневная гигиена.

---

Связь с Явь, Навь, Правь, Ноосфера — архитектура доверия, доказательства и наблюдения

Минимальное доказательство — это Правь в действии. Оно проводит границу:

• Явь — то, что мы доказываем (контракты, инварианты, типы).
• Навь — то, что мы наблюдаем (внешний мир, curl, Б24).
• Правь — само рассуждение, которое связывает их и проводит границу.
• Ноосфера — накопленное знание о том, где границы проходят и где они рвутся.

Когда программист говорит «здесь я не знаю, что вернёт Б24» — он проводит границу. Когда он говорит «здесь я предполагаю, что список непустой» — он формулирует контракт. Когда он говорит «здесь я не проверил, что будет при ошибке» — он видит разрыв в доказательстве.

Всё это — минимальное доказательство. Не Coq. Не Lean. Просто честное рассуждение о том, что код обещает и почему он это выполняет.

---

Практический манифест

1. Каждая функция имеет контракт. Что обещает, при каких условиях. Если не можешь сформулировать — не понимаешь функцию.

2. Каждый цикл имеет инвариант. Что сохраняется на каждой итерации. Если не можешь сформулировать — цикл может делать не то.

3. Каждая граница доверия типизирована. Монада Result, Unknown-ветка, явный контракт. Если не можешь — не знаешь, что вернёт внешний мир.

4. Каждый баг — это разрыв в доказательстве. Не «забыл обработать», а «не сформулировал, что должно быть обработано».

5. Каждое ревью — это проверка доказательства. Не «выглядит нормально», а «докажи, что это работает, и покажи, где граница».

6. Каждое наблюдение пополняет Ноосферу. Баг, пойманный в тесте, — это знание о Нави, которое должно стать общим.

---

Итог

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

• дать язык (контракт, инвариант, граница, неполнота);
• встроить в ритуалы (ревью, коммиты, тесты);
• сделать дешёвым (типы, assert, Unknown);
• показать выгоду (каждый пойманный баг — история успеха);
• встроить в обучение (с первых дней, как гигиену).

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

Явь доказуема. Навь наблюдаема. Правь проводима. Ноосфера разделяема. И минимальное доказательство — это то, что делает Правь ежедневной практикой, а не академическим упражнением.

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

---

Обзор ключевых фигур и ресурсов

---

Конкретные рекомендации по быстрому старту

Если вы хотите начать с самого практичного пути, смотрите работы K. Rustan M. Leino . Он руководил разработкой Dafny в Amazon и создал множество инструментов верификации, используемых в промышленной среде. Канал Verification Corner содержит большое количество вводных материалов и демонстраций, подходит для инженеров, желающих понять, как «доказывать корректность программ на практике».

Если вы хотите понять теоретические основы, отправной точкой является Hoare Logic Tony Hoare . Классическая статья 1969 года «An Axiomatic Basis for Computer Programming» до сих пор является базовой работой по доказательству корректности программ. Позднее он также продвигал инициативу Verified Software Initiative, стремясь распространить крупномасштабную формальную верификацию программ на промышленный уровень.

Если вы хотите учиться на практике через Lean, канал Lipsum dot dev предлагает систематический вводный курс, от определения типов до формальных доказательств алгоритмов сортировки , полностью на французском языке, но содержание демонстраций понятно.

---

Дополнение

Robin Milner, Robert Floyd и другие ушли из жизни, в интернете их выступления в основном представляют собой исторические архивные материалы . Но инструменты и методология, которые они оставили, продолжают развиваться в проектах Dafny, Lean, Rocq (ранее Coq) и других, и за этими проектами стоит активное сообщество разработчиков и исследователей — их каналы и блоги и есть те «живые» каналы, через которые можно получить знания по доказательству корректности.

Программирование