3 ms·
The equivalence seems to hold only when the program is complete. Thus, while all proofs can be expressed as programs, not all programs can be expressed as proo
by sdp 18y ago
The equivalence seems to hold only when the program is complete. Thus, while all proofs can be expressed as programs, not all programs can be expressed as proofs.
- sdp 18y agoPrograms are equivalent to proofs given their correctness, rather. Additionally, according to the wikipedia article, extracting a proof from a program requires a very richly typed programming language.
- 13ren 18y agoCan't you restrict the domain, and so that the program is complete (for that restricted domain)?
- sdp 18y agoI meant correct, not complete. I refer to the article on wikipedia which states: "A converse direction is to use a program to extract a proof, given its correctness. 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."