Curry-Howard correspondence

Remark. Brouwer-Heyting-Kolmogorov (BHK) interpretation makes this correspondence explicit:

• Propositions ~ types.

• Proofs ~ terms inhabiting those types.

• BHK: A proof of $A\to B$ is a function transforming proofs of $A$ into proofs of $B$.

• Program: A term of type $A\to B$ is a function transforming terms of type $A$ to terms of type $B$.