Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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
8  
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 '14 at 20:07
2  
@durron597: Is there a market for such software? Hello world printers, reloaded version? Now with more hellos and more worlds? – JensG May 15 '14 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 '14 at 20:33
9  
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 '14 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 '14 at 16:47
up vote 17 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 uncertainty.

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
6  
Consider the totally type-correct function: int add(int a, int b) { return a - b; } – Donal Fellows May 15 '14 at 20:32
    
@DonalFellows: Which is precisely the reason I included the link about the Ariane 5. – Robert Harvey May 15 '14 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 '14 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 '14 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 '14 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  
+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 '14 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
4  
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 '14 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 '14 at 17:43
    
The space shuttle program used a three independent system voting configuration. Any dissenting votes meant (or, really, suggested) that system was no longer correct, and was taken offline. – jdv Apr 23 at 12:45

A program has some specification and runs in some environment.

(the cosmic ray example in others answers changing add to FireMissiles could be thought part of the "environment")

Assuming you can formally specify the program's intended behavior (i.e. its specification) and its environment, you could sometimes formally prove that the program is -in that precise sense- bug free (so its behavior or output respects the formalization of its specification in the formalization of its environment).

In particular, you might use sound static source analyzers, like e.g. Frama-C.

(but the current state of the art of such analyzers does not permit whole program analysis & proof of large scale programs like the GCC compiler or the Firefox browser or the Linux kernel; and my belief is that such proofs won't happen in my lifetime. I was born in 1959)

However, what you have proved is the correct behavior of the program w.r.t. some particular specification in some (class of) environment(s).

Practically speaking, you could (and NASA or ESA probably wants to) prove that some spacecraft software is "bug free" w.r.t. some precise -and formalized- specification. But that does not mean that your system will always behave like you want.

In simpler words, if your spacecraft robot meet some E.T. and you have not specified that, there is no way to have your robot behave like you really want ....

Read also J.Pitrat's blog entries.

BTW, Halting problem or Gödel's theorem probably applies also to the human brain, or even the human species.

share|improve this answer
    
Perhaps a better example of an SEU changing the call to Add to LaunchMissiles would be an SEU changing some data value that eventually results in an erroneous call to LaunchMissiles. SEUs are a problem with computers that go into space. This is why modern spacecraft oftentimes fly multiple computers. This adds a new set of problems, concurrency and redundancy management. – David Hammen Apr 12 at 17:17

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

There are a lot of good answers here, but they all seem to skirt around the critical point, which is this: all of those theorems have a similar structure and say similar things, and what they say is not "it's impossible to probably write correct programs" (for some specific value of "correct" and "program" that varies in case to case), but what they do say is "it's impossible to prevent somebody writing an incorrect program that we can't prove to be incorrect" (etc).

Taking the specific example of the halting problem, the difference becomes clearer: obviously there are programs that provably halt, and other programs that provably never halt. That there is a third class of programs whose behaviour cannot be determined either way isn't an issue if all we want to do is write a provably-halting program, as we can simply avoid writing a program that belongs to that class.

The same is true with Rice's theorem. Yes, for any non-trivial property of a program we can write a program that can neither have that property proven true nor false; we can also avoid writing such a program because we are able to determine if a program is provable.

share|improve this answer

My answer will be from the perspective of real world business and the challenges that every development team faces. What I see in this question and a lot of the answers is really about controlling defects.

Code can be bug-free. Take any of the "Hello World" code samples for any programming language, and run that on the platform it is intended and it will work consistently and produce the desired results. There ends any theory on the impossibility of code being bug-free.

The potential bugs come in as the logic becomes more complex. The simple Hello World example has no logic and does the same static thing each time. As soon as you add logic-driven dynamic behavior is what introduces the complexity which leads to the bugs. The logic itself can be flawed, or the data that is input to the logic can vary in a way the logic does not handle.

A modern application also depends on run-time libraries, CLR, middleware, database, etc. layers which while saving development time overall, are also layers where bugs within those layers can exist and go undetected through development & UAT testing and into production.

Lastly, the chain of apps/systems that the application consumes data which feed its logic are all sources of potential bugs either within their logic, or within the software stacks the logic rides on top of, or the upstream systems which it consumes data.

Developers are not in 100% control of every moving piece supporting the logic of their application. Actually, we are not in control of much. That is why unit testing is important, and configuration and change management are important processes which we must not ignore or be lazy/sloppy.

Also, documented agreements between your application which consumes data from a source beyond your control, which defines the specific format and specifications for the data transferred, as well as any limit or constraints which your system assumes the source system is responsible for ensuring output is within those bounds.

In the real world application of software engineering you won't be able to make it fly by explaining to the business why theoretically applications cannot be bug-free. Discussions of this nature between technology and the business will never happen except in the aftermath of a technological malfunction which impacted the business's ability to make money, prevent losing money, and/or keeping people alive. The answer to "how can this happen" cannot be "let me explain this theory so you understand."

In terms of massive computations that theoretically could take forever to perform the calculation and get a result, an application that cannot finish and return with a result -- that is a bug. If the nature of the computation is such that it is very time consuming and compute intensive, you take that request and provide feedback to the user how/when they can retrieve the result, and kick off the parallel threads to churn on it. If this needs to happen quicker than can be done on one server, and is business important enough, then you scale it out across as many systems as is needed. This is why cloud is very attractive, and the ability to spin up nodes to take on work and spin them down when done.

If the possibility exists to get a request that no amount of compute power can complete, it should not hang out there running to infinity with a business process waiting on the answer to what the business thinks is a finite problem.

share|improve this answer

I don’t believe code is ever 100% bug free because code is never truly finished. You can always improve on what you write.

Programming is a field of science and math in which case both are endless. The great thing about being a developer is our job is endless.

There are a thousand plus ways to write a single line of code. The idea is to write the most optimized version of that line of code but that may not be bug free. Bug free refers to the idea that your code is unbreakable and all code can be broken in some degree or method.

So can code be efficient? Yes.
Can code be optimized endlessly? Yes.
Can code be bug free? No, you just simply have not found a way to break it yet.
That being said, if you strive to better yourself and your code writing practices, your code will be hard to break.

share|improve this answer
    
this post is rather hard to read (wall of text). Would you mind editing it into a better shape? – gnat Apr 12 at 19:47

protected by gnat Apr 12 at 19:47

Thank you for your interest in this question. Because it has attracted low-quality or spam answers that had to be removed, posting an answer now requires 10 reputation on this site.

Would you like to answer one of these unanswered questions instead?

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