Skip to content
Better HN
Top
Best
Ask
Show
New
Jobs
Search
⌘K
0 points
seanmcdirmid
11y ago
0 comments
Save
Share
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.
0 comments
2 comments · 1 top-level
top
newest
oldest
jsprogrammer
11y ago
· 1 in thread
How do you know there isn't another, yet undiscovered, bug?
seanmcdirmid
OP
11y ago
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.
j
/
k
navigate · click thread line to collapse