Proofs as programs

proofs as programs

The type corresponding to a proposition of the form $\left(\forall x\!:\!A.\ \exists y\!:\!B.\ S[x, y]\right)$ is the function space $x\!:\!A \rightarrow y\!:\!B \times [\![S[x, y]]\!]$. The proof expressions, say p, for this object denotes a canonical element of the type. That element is a function $\lambda(x.b)$ where for each $a \in A, b[a/x] \in y\!:\!B \times [\![S[a, y]]\!]$ and if $1o\!f(b[a/x]) \in B$ and $2o\!f(b[a/x]) \in [\![S[a, 1o\!f(b[a/x])]\!]$. So the function $\lambda(x.\ 1o\!f(b)) \in A \rightarrow B$ and let $f= \lambda(x.\ 1o\!f(b))$, then $f \in A \rightarrow B$ and $\lambda(x.\ 2o\!f(b))$ proves $\forall x\!:\!A.\ S[x, f(x)]$.

So we can see that the process of proving the ``specification'' $\forall x\!:\!A.\ \exists y\!:\!B.\ S[x, y]$ constructively creates a program f for solving the programming task given by the specification, and it simultaneously produces the verification $\lambda(x.\ 2o\!f(b))$ that the program meets its specification (c.f. [29,8] and [70]).