Is there a way to prove a program has no bug?

Question

I was thinking about the fact that we can prove a program has bugs. We can test it to assess that it is more or less bug resistant.

But is there a way (even theoretically) to prove that a program has no bug ?

For simple programs, such as a "Hello World", I guess we should be able to do it. But what about larger programs ?

Secondguess

Not in the general case. Look up the Halting Problem, which is an intuitive proof that it's not even possible to write a program to tell whether another program will ever finish, let alone be bug-free. – Reporter

@Reporter You are saying that it is not possible to prove all correct programs correct. The question is “Is there a way to prove a program has no bug?” and the answer is yes. It is even possible to prove a largish, useful program correct: CompCert. And a second one: seL4. – Pippy

Concerning seL4: Could somebody with 1500+ reputation create a tag "seL4", so it could be added here? Seems there is some work in a seL4 specific Q/A site for stack overflow: area51.stackexchange.com/proposals/120611/sel4 – Garlan

Answer 1

There are nowadays many different formalisms that can be used to prove programs correct (e.g., formalizations in proof assistants, dependently typed programming languages, separation logic, ...). As noted by others, there is no automatic way to prove any given program correct (see the halting problem). However, those mentioned formalisms are often applicable to specific programs. (Such an application can be far from automatic and require a tremendous amount of creativity.)

Another very important point is what we actually mean by proving a program correct or as you stated prove that a program has no bug. Even with formal methods there is typically no way to say that nothing whatsoever can go wrong with a program. The reason is that formal methods usually show that a program conforms to a specification.

You can think of a specification as a logical formula (that states some property about a program) and of the correctness proof as a formal proof that a program satisfies this formula (i.e., enjoys the corresponding property). Due to this setup, everything outside the specification is not even "considered" by the proof. So to really show that a program has no bugs you would first have to write down a logical formula that states when a program does not have bugs.

So it would maybe be more honest to say that formal methods are often able to prove (without doubt) that a program does not have certain kinds of bugs (depending on the used specification).

Horrorstruck