6 ms·
Without knowing much about the topic, when I hear about code being proven to be correct it makes me think of the Curry-Howard correspondence, which states that
by goolulusaurs 5y ago
Without knowing much about the topic, when I hear about code being proven to be correct it makes me think of the Curry-Howard correspondence, which states that proofs and programs are isomorphic to each other. Is this related at all? If programs and proofs are the same thing and you have a proof that a program is correct, is that like having a proof that a proof is correct? In which case it seems like you are getting into the domain of meta-logic.
- skybrian 5y agoNo, not really. Under Curry-Howard, if you have a total function that returns an integer, you’ve proven that an integer exists. But we knew that already. To prove non-trivial things, you need more sophisticated types that make interesting assertions about their values, where it’s not immediately obvious how to construct a value of that type. Special proof languages are used for this.
- fooker 5y agoIt is related, but not in the way you are imagining.