Curry-Howard Isomorphism is an isomorphism between types (in programming languages) and propositions (in logic). Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs (and vice versa).
As is well established by now,
theAnswer :: Integer theAnswer = 42
The logical interpretation of the program is that the type
Integer</haskell> is inhibited (by the value <hask>42), so the existence of this program proves the proposition
Integer (a type without any value is the "bottom" type, a proposition with no proof).