Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

I have read lot of articles which state that code can't be bug-free, and they are talking about these theorems:

Actually Rice's theorem looks like an implication of the halting problem and the halting problem is in close relationship with Gödel's incompleteness theorem.

Does this imply that every program will have at least one unintended behavior? Or does it mean that it's not possible to write code to verify it? What about recursive checking? Let's assume that I have two programs. Both of them have bugs, but they don't share the same bug. What will happen if I run them concurrently?

And of course most of discussions talked about Turing machines. What about linear-bounded automation (real computers)?

share|improve this question
3  
I'm pretty sure this python program does everything it's intended to do and no more: print "Hello, World!"... can you be a bit more clear? –  durron597 May 15 at 20:07
1  
@durron597: Is there a market for such software? Hello world printers, reloaded version? Now with more hellos and more worlds? –  JensG May 15 at 20:31
    
@JensG that's why I asked him to be clear... Saying something like "beyond a certain level of complexity" etc. –  durron597 May 15 at 20:33
2  
None of these theorems have anything to do with bugs or the existence of bug free programs. They are theorems about what questions are answerable by computation. These theorems show that there are some problems that can't be computed, and some mathematical propositions that can neither be proven or disproven, but they certainly don't say that all programs have bugs or that particular programs can't be proved correct. –  Charles E. Grant May 16 at 16:31
1  
In order to prove a program is correct, you'd need a specification that lays out exactly how the program is supposed to act in all cases. I've certainly never seen one of those for any non-trivial program. –  Steven Burnap May 16 at 16:47

5 Answers 5

up vote 11 down vote accepted

It's not so much that programs can't be bug-free; it's that it's very hard to prove that they are, if the program you're trying to prove is non-trivial.

Not for lack of trying, mind you. Type systems are supposed to provide some assurance; Haskell has a highly-sophisticated type system that does this, to a degree. But you can never remove all of the certainty.

Consider the following function:

int add(int a, int b) { return a + b; }

What might go wrong with this function? I already know what you're thinking. Let's say that we've covered all of the bases, like checking for overflow, etc. What happens if a cosmic ray strikes the processor, causing it to execute

LaunchMissiles();

instead?

OK, maybe that's a bit contrived. But even simple functions like the add function above must operate in environments where the processor is constantly changing contexts, switching between multiple threads and cores. In an environment like that, anything can happen. If you doubt this, then consider that RAM is reliable, not because it is error free, but because it has a built-in system to correct the bit errors that inevitably occur.

I know what you're thinking. "But I'm talking about software, not hardware."

There are many techniques that can improve your confidence level that the software works the way it is supposed to. Functional programming is one of them. Functional programming allows you to better reason about concurrency. But functional programming is not a proof, any more than unit tests are.

Why? Because you have these things called edge cases.

And once you get only a little beyond the simplicity of return a + b, it becomes remarkably difficult to prove a program's correctness.

Further Reading
They Write the Right Stuff
The Ariane 5 Explosion

share|improve this answer
4  
Consider the totally type-correct function: int add(int a, int b) { return a - b; } –  Donal Fellows May 15 at 20:32
    
@DonalFellows: Which is precisely the reason I included the link about the Ariane 5. –  Robert Harvey May 15 at 20:34
2  
@DonalFellows - Mathematical characterisation does not solve the problem, it only moves it elsewhere. How do you prove that the mathematical model actually represents the client need? –  mouviciel May 16 at 14:53
1  
@JohnGaughan That assumes interdependencies between the modules. Given modules that have been proved correct and proved independent of one another, you can recursively compose them into larger modules that are also known to be correct and independent ad infinitum. –  Doval May 16 at 15:23
1  
@JohnGaughan If the integration of modules causes bugs then you've failed to prove they're independent. Building new proofs out of established proofs isn't any harder than building proofs out of axioms. If mathematics got exponentially harder that way, mathematicians would be screwed. You could have bugs in your build scripts, but that's a separate program. There's no mystery element that goes wrong when you try to compose things, but depending on the number of side effects it can be difficult to prove there's no shared state. –  Doval May 16 at 16:35

First, let's establish what context you wish to discuss this in. The Programmers Q&A at Stack Exchange suggests that you are most likely interested in the real world existence of tools / languages rather than theoretical results and Computer Science theorems.

I have read lot of articles which state that code can't be bug-free

I hope not, because such a statement is incorrect. Though it is commonly accepted that most large-scale applications are not bug-free to the best of my knowledge and experience.

More commonly accepted is that there does not exist (i.e. existence, not possibility) a tool that perfectly determine whether a program written in a Turing-complete programming language is completely bug free.

A non-proof is a intuitive extension of the Halting Problem, combined with the observation data of everyday experience.

There does exist software that can do "proofs of correctness" that verify that a program meets the corresponding formal specifications for the program.

Does this imply that every program will have at least one unintended behavior?

No. Though most applications have been found to have at least one bug or unintended behavior.

Or does it mean that it's not possible to write code to verify it?

No, you can use formal specifications and proof assistants to verify following the specification, but as experience has shown mistakes can still exist in the overall system, such as factors outside the specification - the source code translator & hardware, and most frequently mistakes are made in the specifications themselves.

For more gory details, see Coq is such a tool / language / system.

What about recursive checking?

I don't know. I'm not familiar with it, and I'm not sure if it is a computability problem or a compiler optimization problem.

share|improve this answer
    
+1 for being the first talking about formal specifications and proof assistants. This is a crucial point, which is missing in the previous answers. –  MainMa May 16 at 19:01

I want to ask, does it imply that every code will get at least one unintended behaviour?

No. Correct programs can be and are written. Mind you, a program can be correct, but it's execution may fail due to, eg, physical circumstances (as the user Robert Harvey wrote in his answer here), but this is a distinct matter: that program's code is still correct. To be more precise, the failure is not caused by a fault or error in the program itself, but in the underlying machine that executes it (*).

(*) I am borrowing definitions for fault, error and failure from the dependability field as, respectively, a static defect, an incorrect internal state, and an incorrect external observed behavior according to its specification (see <any paper from that field>).

Or, does it mean that I am not able to write code, which will check it?

Refer to the general case in the statement above and you are correct.

You may be able to write a program that checks if a specific X program is correct. For example, if you define a "hello world" program as one with two instructions in sequence, namely print("hello world") and exit, you can write a program that checks if its input is a program composed of these two instructions in sequence, thus reporting if it is a correct "hello world" program or not.

What you can't do using current formulations is to write a program to check if any arbitrary program halts, which implies the impossibility of testing for correctness in the general cases.

share|improve this answer

Running two or more variants of the same program is a well-known fault tolerance technique called N-variant (or N-version) programming. It is an acknowledgement of the presence of bugs in software.

Usually these variants are coded by different development teams, using different compilers, and sometimes are executed on different CPUs with different OSes. Outcomes are voted before being output to the user. Boeing and Airbus love this kind of architecture.

Two weak links remain, leading to common mode bugs:

  • There is only one specification.
  • the voting system is either unique or complex.
share|improve this answer
1  
I believe NASA or other space program have suggested that N-variant suffers from the problem that too often programmers think alike and thus end up independently writing near equivalent programs with common flaws when the flaw is beyond the most trivial level. For example, refer to the same reference information (see long standing bug in binary search ), tend to use the same algorithms, and make the same sorts of mistakes. –  mctylr May 20 at 16:33
    
@mctylr - It's a very good point. But actually, until recently, there was not enough room in memory to store more than one variant of a software on a spacecraft. Their answer is test, test, test, rinse, repeat. –  mouviciel May 20 at 17:43

Does this imply that every program will have at least one unintended behavior?

No.

The halting problem says that it's impossible to write a program that tests whether every program halts in a finite amount of time. This does not mean that its impossible to write a program that can categorize some programs as halting, some others as non-halting. What it means is that there are always will exist some programs that a halting analyzer cannot categorize one way or the other.

Gödel's incompleteness theorems have a similar gray area to them. Given a mathematical system of sufficient complexity, there will exist some statements made in the context of that system whose veracity cannot be assessed. This does not mean mathematicians have to give up on the idea of proof. Proof remains the cornerstone of mathematics.

Some programs can be proven to be correct. It's not easy, but it can be done. That is the goal of formal theorem proving (a part of formal methods). Gödel's incompleteness theorems do strike here: Not all programs can be proven to be correct. That does not mean it is utterly futile to use formal methods because some programs can indeed be formally proven to be correct.

Note: Formal methods preclude the possibility of a cosmic ray striking the processor and executing launch_missiles() instead of a+b. They analyze programs in the context of an abstract machine rather than real machines that are subject to single event upsets such as Robert Harvey's cosmic ray.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.