Sunday, July 17, 2011

A Theory of Bugs, or: a New Model for Proof-Checking

Yuval Peres, who was the secret influence behind the recent shift of
Computer Science conferences towards mandating that full proofs be
included in the appendix of submissions, has a theory about bugs. He
likes to say that, more often than not, mistakes lie in the parts of
a proof that have been given less attention than the rest, and that
in the manuscript, such parts are often prefaced by wording such as:
"It is easy to see that...". Those words are like a red flag.

Such a theory makes for interesting lunch time conversations, but, as
creationists like to say about the theory of evolution with a
dismissive, contemptuous tone of voice: "It's just that, a mere
theory" - implying that it therefore has no value.

Very recently Yuval's Theory of Bugs was validated by real events. An
exciting new result came out. Yuval was interested, but suspicious
(as one always should be with exciting results), but too busy to
check the proof for correctness line by line. So, he applied his
theory, and searched for the sentence: "It is easy to see". No luck.
Then he searched for: "It is easy to verify", and found one instance.
He focused on that claim, and, sure enough! The claim was flawed --
in fact it was easy for him to verify, not that the claim was true,
but that the claim was false.

No comments:

Post a Comment