The Curry-Howard isomorphism is the correspondence between type systems (like for the simply typed lambda calculus) and proof systems (like natural deduction). More precisely, types resemble propositions, terms resemble proofs, reduction resembles cut elimination etc.
The isomorphism becomes obvious because there is a 1-to-1 correspondence between the inference rules of Curry typing and the inference rules of predicate logic ND systems, for example.
However, what is not obvious (to me) is why this happens. Is there a deeper reason that proofs and typing are just two facets of the same system?
Merely noting that this is possible because the basic definitions are isomorphic is not really satisfactory, because this just shifts the question towards asking why the definitions of these systems end up isomorphic.