I 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 correc

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