«Запустилось без ошибок» — не значит «верно». Верно — значит соответствует спецификации, и это можно доказать. Здесь математическая логика входит в код напрямую: по соответствию Карри-Ховарда тип — это утверждение, а программа — его доказательство. Дальше — тотальность, инварианты и спектр способов получить уверенность.
Программа корректна не тогда, когда «работает на моих примерах», а когда делает ровно то, что обещано спецификацией — для всех допустимых входов. Это смещает планку: вместо «запустилось без ошибок» — «доказано, что соответствует». А раз речь о доказательстве, в дело вступает математическая логика: корректность программы — это теорема, которую нужно установить.
Функциональный подход из главы VI дал для этого почву: чистота и неизменяемость делают рассуждение локальным, а значит — поддающимся доказательству. Теперь добавим инструменты строгости: типы, тотальность и собственно доказательства.
Соответствие точное. Функция $A\to B$ — это импликация: имея $A$, получаем $B$. Произведение — конъюнкция, сумма — дизъюнкция, единичный тип — истина, пустой — ложь:
$A\to B \;\equiv\; A\Rightarrow B,\qquad A\times B \;\equiv\; A\wedge B,\qquad A + B \;\equiv\; A\vee B$
Практический смысл огромен: система типов — это лёгкий доказатель. Если программа прошла проверку типов, часть свойств уже доказана машиной, а не «проверена на глаз». Чем выразительнее типы, тем больше теорем они способны нести — вплоть до полной спецификации.
Делать функции тотальными — дисциплина: исчерпывающе разобрать все случаи (отсюда польза сумм-типов из углубления об алгебраических типах) и моделировать частичность явно — возвращать Maybe/Result вместо исключения. Языки с проверкой тотальности (например, Idris) прямо отмечают, тотальна ли функция. В Elixir это идиома честного результата:
Property-based testing — золотая середина: вместо отдельных примеров формулируют свойство-инвариант и проверяют его на сотнях сгенерированных входов. На вершине — помощники доказательств и зависимые типы (Lean, Agda, Idris, Rocq, бывший Coq): тип может зависеть от значения, и тогда спецификация записана прямо в типе, а компилятор её доказывает.
Классический пример — вектор с длиной в типе. Сложив векторы длины $n$ и $m$, получаем вектор длины $n+m$ — и это записано прямо в сигнатуре. Компилятор доказывает совпадение длин, поэтому случай несовпадения не нужно обрабатывать: он невозможен.
Так инвариант («длины складываются») перестаёт быть комментарием и становится теоремой, проверенной машиной. Это и есть мост из углубления об алгебраических типах: сделать недопустимое невыразимым — и доказать допустимое.
• Запрет недопустимых состояний (сумма-типы).
• Гарантию обработки всех случаев (тотальность).
• Доказательство числовых и структурных инвариантов (зависимые типы).
Даже без зависимых типов полиморфная сигнатура ограничивает поведение: по типу $\forall a.\ a\to a$ функция может быть только тождеством. Тип говорит о программе больше, чем кажется.
Корректность — это соответствие спецификации, установленное доказательством. По Карри-Ховарду тип есть утверждение, а программа — его доказательство; тотальность делает функции честными; спектр от типов через property-тесты до зависимых типов даёт уверенность под цену ошибки; инварианты, записанные в типах, доказываются машиной. Логика вошла в код.
И здесь — ответ на тезис финала: именно так со сложностью можно не сражаться. Когда инварианты, логика и доказательства под рукой, не нужно держать всё в голове — за корректность ручается тип. Дальше — глава о том, что математика становится общим языком человека и нейросети.