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$.