В чём заключается соответствие Карри — Говарда?

Соответствие Карри — Ховарда (изоморфизм Карри — Ховарда) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами. ru.ruwiki.ru ru.wikipedia.org

Суть соответствия в том, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины. ru.ruwiki.ru ru.wikipedia.org

В современном представлении соответствие Карри — Ховарда не ограничивается какой-то одной логикой или системой типов. ru.ruwiki.ru Например, логика высказываний соответствует простому типизированному λ-исчислению, логика высказываний второго порядка — полиморфному λ-исчислению, исчисление предикатов — λ-исчислению с зависимыми типами. ru.ruwiki.ru

Использование соответствия Карри — Ховарда позволило создать класс функциональных языков программирования, среда выполнения которых одновременно является системой автоматического доказательства, таких как Coq, Agda и Epigram. ru.ruwiki.ru ru.wikipedia.org