Theoretically bug-free programs

Question

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

• Halting problem
• Gödel's incompleteness theorem
• Rice's theorem

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)?

Answer 1

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

Answer 2

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.

Answer 3

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.

Answer 4

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.

Answer 5

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.

Answer 6

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.

Answer 7

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.

Answer 8

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.

Answer 9

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.