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".