3 ms·
Can't you restrict the domain, and so that the program is complete (for that restricted domain)?
by 13ren 18y ago
Can'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."