4 ms·
Coq 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.
by Joof 11y ago
Coq 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?