proof that "all software has bugs?"

[westfalr]

When I Google "all software has bugs," I get over 400,000 pages. Also I've heard somewhere that this has been proven.

 

If it has, by who, and where can I find a copy of the proof?

[Mokele]

It's pretty easy to disprove - get any "intro to programming" book and write the "Hello World" program they all invariably have as the first example.

[bascule]

Actually, quite the opposite is true. It's possible to formally prove that certain programs are correct, using techniques like model checking, for example:

 

http://en.wikipedia.org/wiki/Formal_methods#Automated_proof

[westfalr]

OK the statement is wrong as given. But why do so many people say it? If the quoted phrase pops up 400K times in Google, you'd think that somebody said something somewhere that somehow established the phrase in people's minds.

 

Perhaps I should check Internet rumor sites. Maybe it came from a chain letter.

 

Thinking about it, the adjective nontrivial may have been in the statement. But who knows what that means?

[Mokele]

Well, most software that is actually *useful*, especially useful enough to be commercially viable, is vastly more complex than the simple example I gave. And as things get more complex, errors become more and more likely.

[D H]

When I Google "all software has bugs," I get over 400,000 pages. Also I've heard somewhere that this has been proven.

 

As noted earlier, that statement is provably false. However, most useful software products are buggy. A "Hello, world" program isn't very useful. A useful program such as the one that drives this website almost certainly has bugs.

 

The formal methods to which Bascule alluded are not all that useful, either. Employing them is a very expensive process, they can only be used on certain types of software, and the kinds of people who are adept at formal methods are generally clueless at the domain level while people who know the domain are generally clueless regarding the requisite logic behind formal methods. I have seen formal methods deployed once in my thirty years of work, regarding a communications device that works with multi-security level data.

[bascule]

I have seen formal methods deployed once in my thirty years of work, regarding a communications device that works with multi-security level data.

 

I saw a demonstration of model checking recently, using McErlang. They formally verified that a real-world piece of elevator control software was correct (and found some bugs along the way, I believe).

[ajb]

I'd take the statement "all software has bugs" to be a rough metatheorem of computer science, meaning (as already alluded to) "any useful software is going to have some bugs".

 

It means on a practical level any complex software written is likely to have at least one bug. This is mostly due to human error*, rather than any "fundamental" principle in computer science. Thus I'd take it to mean "we all make mistakes".

 

 

* I am assuming that there does exist at least one algorithm finite in time that will implement what the software is designed to do.

[hobz]

Without defining the term "bug" more ridigly, I would suggest that the calculator that comes bundled with Windows XP is useful and bugless.

[NeonBlack]

I'd take the statement "all software has bugs" to be a rough metatheorem of software engineering, meaning (as already alluded to) "any useful software is going to have some bugs".

 

Computer science has nothing to do with useful software.

[Mr Skeptic]

Consider all the books and textbooks you've read. No doubt you find typos and even mistakes once in a while -- "bugs" if you will. Computer code is harder than that, since it does all sorts of stuff, frequently is made by several different people, and very self-referential. For example, you typically make several functions or objects and use them repeatedly, which is roughly comparable to inventing new (completely unambiguous) words and writing most of your book with those new words. Since computers suck at dealing with ambiguity, any ambiguities that are resolved in a way the programmers did not intend is also a bug. Large portions of the code are often loops, meaning they run repeatedly with different parameters. Basically, you can't "proof read" the program as you would a book because you would never be able to read the whole thing as the computer would, as you would have to re-read things thousands of times and keep track of what each variable is at that time.

 

You can almost guarantee there will be several mistakes, and hope that the worst ones are caught. Programs can be made bug-free, but that is absurdly expensive.

[ajb]

Computer science has nothing to do with useful software.

 

I am sure there is plenty of overlap between the two disciplines.

[bascule]

I am sure there is plenty of overlap between the two disciplines.

 

I'm sure the remark was a facetious stab at the fact that computer science spends far too much time concerning itself with theory and too little with practical application.

[padren]

OK the statement is wrong as given. But why do so many people say it? If the quoted phrase pops up 400K times in Google, you'd think that somebody said something somewhere that somehow established the phrase in people's minds.

 

"Every home has it's quirks" doesn't imply that literally, every home must, by definition contain at least one (oh wait, plural, make that) two or more quirks. It means you should expect quirks when you buy a home. Likewise, you should expect software to contain potential bugs.

 

"There is no such thing as an unloaded gun" is similar but more cautionary example. It really has more to do with conventional wisdom than computer science, though it is true that statistically it is highly probable that any given piece of useful software will contain bugs.

[bascule]

OK the statement is wrong as given. But why do so many people say it? If the quoted phrase pops up 400K times in Google, you'd think that somebody said something somewhere that somehow established the phrase in people's minds.

 

Most code is not written in a manner which can be proven correct through model checking, let alone written in a language where model checking can be used to demonstrate formal correctness, and even when it is, who actually subjects their code to model checking? In practice very little code is provably correct.

[fiveworlds]

who actually subjects their code to model checking?

 

Sometimes.

 

In practice very little code is provably correct.

 

Not really you have validators that do a pretty good job of making sure your code is correct. Also most integrated development environment have all sorts of error checking methods programmed in to highlight potential errors. Even notepad++ has error checking and code suggestion for tons of languages.

Edited March 18, 2016 by fiveworlds

[John Cuthber]

Can you get code that checks the date of a post before you reply to it?

[fiveworlds]

Oops didn't look to be honest I just saw the thread link on the main page.

[Unity+]

Computer science has nothing to do with useful software.

On the contrary, computer science has everything to do with useful software.

I'm sure the remark was a facetious stab at the fact that computer science spends far too much time concerning itself with theory and too little with practical application.

A majority of theory in computer science is based on the formation of logic and mathematics. Unlike physics, where theory is based on our current understanding of the Universe, computer science concerns itself with the axioms formulated within mathematics to produce algorithms based on such axioms.

[Strange]

 

Sometimes.

 

 

Not really you have validators that do a pretty good job of making sure your code is correct. Also most integrated development environment have all sorts of error checking methods programmed in to highlight potential errors. Even notepad++ has error checking and code suggestion for tons of languages.

 

Those are (largely) just checking for syntactical correctness. They do little or no semantic validation.

 

Formal validation of code written hardware description languages (effectively, software that will be compiled into the design of a silicon chip) is commonly done. This is because of the huge manufacturing costs and the difficulty of replacing faulty hardware. Because it costs almost nothing to distribute buggy software and the issue updates, there is no incentive to be as careful with most software. (Embedded software is treated a little more seriously.)

Can you get code that checks the date of a post before you reply to it?

 

I think the thread was revived by a spammer. (And it is quite an interesting subject...)

Edited March 19, 2016 by Strange

[John Cuthber]

Actually, no software has bugs- the computer does exactly what you tell it to.

The problem is that you are running the wrong software for the job you want to do.

It's a specification problem.

[Strange]

It may be a specification problem. But is more often an implementation problem: the code doesn't match the specification. Or it could be a compiler bug.

 

On the other hand, as most code (rather depressingly) seems to get written without a specification, maybe you are right. And, of course, with no specification there is little scope for formal validation. You could check some properties that should be true for all programs (memory leaks, all memory accesses are valid, etc) but you couldn't check that the program is "correct".

 

Of course, just having a specification (even without any attempt at formal validation) will improve the quality of the code and shorten development time. Which is why it astounds me that so many companies don't do it. The number of times I have had the "It will shorten development time" "But we don't have time" "But it will save you more time than you spend" "I'm sure it will but we just don't have time" conversation is staggering.

[John Cuthber]

Well, since we are currently writing the specification for the piece of software we launched in August...

[Strange]

Ha. I once had to rewrite the user guide for a new product as a requirements spec because the new marketing man said we couldn't have a product without requirements.

[John Cuthber]

For what it's worth, I already wrote the user guide. Now all we need is the spec.