The Curry–Howard correspondence is the observation that there is an isomorphism between the proof systems, and the models of computation. It is the statement that these two families of formalisms can be considered as identical. In normal terms, proving something is the same as describing an algorithm to compute it. That is, a proof is the same as a program. My personal interpretation is that a well-formed program is one for which an isomorphism to a proof has been shown.