Why can't programs be proven?

Question

Proofs are programs.

Formal verification of programs is a huge research area. (See, for example, the group at Carnegie Mellon.)

Many complex programs have been verified; for example, see this kernel written in Haskell.

Programs absolutely can be proven to be correct. Lousy programs are hard to prove. To do it even reasonably well, you have to evolve the program and proof hand-in-hand.

You can't automate the proof because of the halting problem. You can, however, manually prove the post-conditions and preconditions of any arbitrary statement, or sequence of statements.

You must read Dijsktra's A Discipline of Programming.

Then, you must read Gries' The Science of Programming.

Then you'll know how to prove programs correct.

Just a small comment to those who brought up incompleteness -- it is not the case for all axiomatic systems, only sufficiently powerful ones.

In other words, Godel proved that an axiomatic system powerful enough to describe itself would necessarily be incomplete. This doesn't mean it would be useless however, and as others have linked to, various attempts at program proofs have been made.

The dual problem (writing programs to check proofs) is also very interesting.

You can in fact write provably correct programs. Microsoft, for example, has created an extension of the C# language called Spec# which includes an automated theorem prover. For java, there is ESC/java. I'm sure there are many more examples out there.

(edit: apparently spec# is no longer being developed, but the contract tools will become part of .NET 4.0)

I see some posters hand-waving about the halting problem or incompleteness theorems which supposedly prevent the automatic verification of programs. This is of course not true; these issues merely tell us that it is possible to write programs which cannot be proven to be correct or incorrect. That does not prevent us from constructing programs which are provably correct.