For more than a decade I have been systematically identifying error-prone
programming habits—by reviewing the literature, by analyzing other people’s
mistakes, and by analyzing my own mistakes—and redesigning my programming
environment to eliminate those habits. For example, “escape” mechanisms, such
as backslashes in various network protocols and % in printf, are error-prone:
it’s too easy to feed “normal” strings to those functions and forget about the
escape mechanism.
I switched long ago to explicit tagging of “normal” strings;
the resulting APIs are wordy but no longer error-prone. The combined result of
many such changes has been a drastic reduction in my own error rate.
Starting in 1997, I offered $500 to the first person to publish a verifiable
security hole in the latest version of qmail, my Internet-mail transfer agent; see
http://cr.yp.to/qmail/guarantee.html. There are now more than a million
Internet SMTP servers running qmail. Nobody has attempted to claim the $500.
Starting in 2000, I made a similar $500 offer for djbdns, my DNS software;
see http://cr.yp.to/djbdns/guarantee.html. This program is now used to
publish the IP addresses for two million .com domains: citysearch.com, for
example, and lycos.com. Nobody has attempted to claim the $500.
There were several non-security bugs in qmail, and a few in djbdns. My
error rate has continued to drop since then. I’m no longer surprised to whip up
a several-thousand-line program and have it pass all its tests the first time.
Bug-elimination research, like other user-interface research, is highly nonmathematical.
The goal is to have users, in this case programmers, make as few
mistakes as possible in achieving their desired effects. We don’t have any way
to model this—to model human psychology—except by experiment. We can’t
even recognize mistakes without a human’s help. (If you can write a program
to recognize a class of mistakes, great—we’ll incorporate your program into
the user interface, eliminating those mistakes—but we still won’t be able to
recognize the remaining mistakes.) I’ve seen many mathematicians bothered by
this lack of formalization; they ask nonsensical questions like “How can you prove
that you don’t have any bugs?” So I sneak out of the department, take off my
mathematician’s hat, and continue making progress towards the goal.
http://cr.yp.to/cv/activities-20050107.pdf (apparently this guy’s accomplishments are legendary in crypto circles)