Sad truth about programming

There is no such thing as a bug free software. Today I stumbled on this:
http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html
This is an unfortunate and sad truth about programming: regardless of our efforts, software will have bugs; it will crash, it will burn, it will fail. At the same time there is a hope:
http://alloy.mit.edu/
We desperately need code verification tools like this.

This entry was posted in Programming. Bookmark the permalink.

6 Responses to Sad truth about programming

  1. Mimi says:

    I don’t really think that the linked article is worth much.
    First it shows a program with a very basic integer overflow that is said to have stayed undetected for two decades. I can’t believe this since I spotted it right away (my job is to do security code review for sensitive applications).
    Second the article says that you should build test cases for any code you write. What a shocking news.
    Nothing to see here.

  2. Shura says:

    The statement that proving that a program is correct is not sufficient strikes me as rather strange. Of course it’s enough to prove that a program is correct; you just have to make sure that you actually prove it for the language you are using, rather than an idealised version of that language.
    In other words, you have to make sure that the proof actually applies to your code. It may not always be obvious whether it does, but if the proof *is* valid, then your program is bug-free – or, put another way, if your program isn’t bug-free, then the proof wasn’t valid. A situation where you prove a program correct and it still contains bugs is not possible, though, unless you actually made a mistake in formulating the statement you were trying to prove.

  3. Ilfak Guilfanov says:

    Shura,
    Even making sure that the proof actually applies to your code is not enough. The next place for making mistakes is what you prove. Formulating what theorems to prove is error prone.
    The Alloy tutorial clearly demonstrates it: even the simplest cases require careful and elaborate assertions. Two more problems arise: underconstraining and overconstraining the model. I doubt an ideal solution exists but the automatic program verification is a huge step forward. We might need to switch to provable programming languages, though.

  4. Gabriel Gonzalez says:

    Keeping in mind that the bug-free software you are talking about is from a requirements point of view

  5. Software tester says:

    Over-all, there are people who should not
    write software, unless they know what their doing. 80 precent of software on the market today is crap.

  6. Ilfak Guilfanov says:

    I wouldn’t be so harsh. Overall software quality is much better than ten years ago.