3 ms·
> I now sometimes think of a very strict compiler for mathematics that catches errors from the math lingua. Is that what Coq (https://en.wikipedia.org/wiki/Coq
by irremediable 11y ago
> I now sometimes think of a very strict compiler for mathematics that catches errors from the math lingua.
Is that what Coq (https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq) is?
- Joof 11y agoCoq is either too immature or too strict. Writing a proof in coq is far too difficult for what it does. I agree that we need a proof 'compiler' though.
- irremediable 11y agoThanks for the insight on this, by the way; I'm more of an applied math person, so I have no firsthand experience of things like computer-verified proofs, Coq, etc. What do you think are the specific ways in which a proof compiler would be different?