You can re-run your proofs once the bug is patched, so its not like this makes a... | Hacker News

Hacker News new | past | comments | ask | show | jobs | submit

login

seanmcdirmid on March 24, 2015 | parent | context | favorite | on: Proving false in Coq using an implementation bug

You can re-run your proofs once the bug is patched, so its not like this makes all those proofs useless. Actually, that is the nice thing about Coq.

jsprogrammer on March 25, 2015 [–]

How do you know there isn't another, yet undiscovered, bug?

seanmcdirmid on March 25, 2015 | [–]

You don't, but so what? Even proofs done well by hand can have obscure mistakes; most of the time they don't invalidate the proof. Take a proof as strong evidence of correctness and it all works out from a epistemological point of view.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact