Editing Curry–Howard correspondence (section)

== Origin, scope, and consequences == <!--This heading is used in other articles. Please update the links in the other articles if the heading name changes. -->

The beginnings of the '''Curry–Howard correspondence''' lie in several observations:
# In 1934 [[Haskell Curry|Curry]] observes that the [[typed lambda calculus|type]]s of the combinators could be seen as [[axiom-scheme]]s for [[intuitionism|intuitionistic]] implicational logic.{{sfn|Curry|1934}}
# In 1958 he observes that a certain kind of [[proof calculus|proof system]], referred to as [[Hilbert-style deduction system]]s, coincides on some fragment with the typed fragment of a standard [[model of computation]] known as [[combinatory logic]].{{sfn|Curry|Feys|1958}}
# In 1969 [[William Alvin Howard|Howard]] observes that another, more "high-level" [[proof calculus|proof system]], referred to as [[natural deduction]], can be directly interpreted in its [[intuitionistic]] version as a typed variant of the [[model of computation]] known as [[lambda calculus]].{{sfn|Howard|1980}}

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.

If one abstracts on the peculiarities of either formalism, the following generalization arises: ''a proof is a program, and the formula it proves is the type for the program''. More informally, this can be seen as an [[analogy]] that states that the [[return type]] of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem.  This sets a form of [[logic programming]] on a rigorous foundation: ''proofs can be represented as programs, and especially as lambda terms'', or ''proofs can be '''run'''''.

The correspondence has been the starting point of a large range of new research after its discovery, leading to a new class of [[formal system]]s designed to act both as a [[proof calculus|proof system]] and as a typed [[programming language]] based on [[functional programming]]. This includes [[Martin-Löf]]'s [[intuitionistic type theory]] and [[Thierry Coquand|Coquand]]'s [[calculus of constructions]] (CoC), two calculi in which proofs are regular objects of the discourse and in which one can state properties of proofs the same way as of any program. This field of research is usually referred to as modern [[type theory]].

Such [[typed lambda calculus|typed lambda calculi]] derived from the Curry–Howard paradigm led to software like Rocq in which proofs seen as programs can be formalized, checked, and run.

A converse direction is to ''use a program to extract a proof'', given its [[program correctness|correctness]]—an area of research closely related to [[proof-carrying code]]. This is only feasible if the [[programming language]] the program is written for is very richly typed:  the development of such type systems has been partly motivated by the wish to make the Curry–Howard correspondence practically relevant.

The Curry–Howard correspondence also raised new questions regarding the computational content of proof concepts that were not covered by the original works of Curry and Howard. In particular, [[classical logic]] has been shown to correspond to the ability to manipulate the [[continuation]] of programs and the symmetry of [[sequent calculus]] to express the duality between the two [[evaluation strategy|evaluation strategies]] known as call-by-name and call-by-value.

Because of the possibility of writing non-terminating programs, [[Turing completeness|Turing-complete]] models of computation (such as languages with arbitrary [[Recursion (computer science)|recursive functions]]) must be interpreted with care, as naive application of the correspondence leads to an inconsistent logic.  The best way of dealing with arbitrary computation from a logical point of view is still an actively debated research question, but one popular approach is based on using [[Monad (functional programming)|monads]] to segregate provably terminating from potentially non-terminating code (an approach that also generalizes to much richer models of computation,<ref>{{Citation|first=Eugenio|last=Moggi|year=1991|title=Notions of Computation and Monads|journal=Information and Computation|volume=93|issue=1|url=http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf|doi=10.1016/0890-5401(91)90052-4|pages=55–92|doi-access=free}}</ref> and is itself related to modal logic by a natural extension of the Curry–Howard isomorphism<ref name=PfenningDaviesJudgmental group=ext/>). A more radical approach, advocated by [[total functional programming]], is to eliminate unrestricted recursion (and forgo [[Turing completeness]], although still retaining high computational complexity), using more controlled [[corecursion]] wherever non-terminating behavior is actually desired.