Seonglae ChoProofs as programs, propositions as types
The principle that proofs and programs correspond structurally. The core slogan is "proofs as programs, propositions as types" — that is, a proposition is a type, and a proof is a program of that type.
For example, in logic corresponds to the function type
A -> B in programming, to product/tuple types, and to sum/union types.Curry–Howard correspondence
In programming language theory and proof theory, the Curry–Howard correspondence is a direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#External_links