4 ms·
This bug only effects proofs that use types with more than 256 constructors. Also, it involves a command that is meant to optimize proofs so it isn't neccessary
by anonlastname 8y ago
This bug only effects proofs that use types with more than 256 constructors. Also, it involves a command that is meant to optimize proofs so it isn't neccessary to ever use it. Personally, I still trust the implementation despite this edge case.
- anonfirstlasr 8y agoPerhaps this is funny, ironic or simply sarcastic. In any of these cases it’s an empty argument. If you want to criticise formal methods then you should rightly present a cogent argument, or simply stay quiet.
- archgoon 8y agoI believe this comment is meant to be a response to another post (https://news.ycombinator.com/item?id=18155410 https://news.ycombinator.com/item?id=18155410) who pointed out a flaw (now fixed) in Coq that allowed false theorems to be proved. Github link: https://github.com/clarus/falso https://github.com/clarus/falso