Подскажите популярно про Curry-Howard correspondence

[Dims]

Существует соответствие между доказательствами и программами и называется оно "изоморфизм Карри-Ховарда". Только вот я что-то не пойму, что именно чему именно соответствует? Нельзя ли пояснить на простом и наглядном примере доказательства чего-нибудь простого.

Только не вот этого (β → α) → (γ → β) → γ → α, а то я не понимаю, что это такое

Может быть, на примере какой-нибудь простой геометрической теоремы.