Why is it impossible to prove software to be correct?

Question

I heard that computer programs can't be proved to be correct, only tested. Could anyone explain to a math student who knows logic and how to prove theorems in mathematics that why is this impossible? Why can't we for example use Curry-Howard correspondence to convert code to the mathematical theorems and prove them? Or is is because Gödel's theorem says something like there are theorems in an axiomatic system that can't be proved in this concept but can be proved in a larger system?

Answer 1

Whatever you heard is false. Proving programs correct is not only possible, it is also done in practice on large scale. There is an entire branch of computer science, namely formal methods which addresses correctness of programs by mathematical tools.

To give you just a couple of examples:

1. ComCert - formally proved correct optimizing C compiler, as well as the hardware model to which it compiles.

2. Iris - a tool for proving correctness of concurrent programs.

If you search for "formal verification of critical software" you will find many more examples.

And before anyone starts talking about Gödel incompleteness and Halting problem – in the present context those are just red herrings.

Answer 2

I'm wondering if you've misheard or heard a distorted version of the Donald Knuth Quote:

Beware of bugs in the above code; I have only proved it correct, not tried it.'

There is definitely some sort of misunderstanding here, so I'll try to clarify:

1. Can you prove programs correct? Yes, absolutely.

   You're absolutely on the right track with the Curry-Howard stuff. There is a whole field of computer science dedicated to proving programs correct, namely formal methods. There's automated correctness proving (like model checking, SMT, etc.), program logics (like Iris, separation logic, Hoare logic, etc.), and dependent type systems (like Lean, Coq, Agda, Idris, etc.) All of these involve proving a program correct in some way, and all are areas of both theoretical and practical research.

   In fact, if you publish a paper about a new algorithm, you would have a hard time being taken seriously if you didn't give a proof of correctness, or at least a sketch. Proving things correct is a key part of the foundations of computer science.

2. Can you look at a program and determine if it's correct or not? No, not in general. Rice's theorem says that the only things we can determine about a program are those that are syntax-dependent. Any property that is purely semantic or behavioural is undecidable.

   That just means that any program analysis is either conservative or unsound. You can write an analysis that gives a yes/no answer for correctness, but you either have "no actually means maybe" or "yes actually means maybe".

3. Are program correctness proofs meaningful? Maybe.

   It's possible that whoever said you can't prove programs correct was talking about the divide between theory and practice. Programs are always correct relative to (1) a specification and (2) a model of computation.

   For (1), if your specification is wrong, then your program can be "wrong" despite a proof that it meets the specification. This always seemed unlikely to me, that you would have a mistake in the spec, a program meeting the wrong spec, and a proof of that, and not notice the mistake at some point. But it is a true criticism.

   For (2), there are lots of ways that a correctness proof can miss real life details. Are there bounds on memory? Are there possible unexpected side effects? Is the compiler correct (see, for example, Reflections on Trusting Trust ). None of these make proofs useless, and there are efforts by researchers to broaden models to include these things, like the DeepSpec project or the CompCert compiler. But it does mean that a proof of correctness doesn't mean the absence of real world faults.