Why can't programs be proven?

math theory proof axiom formal-verification
4thSpace picture 4thSpace · Jan 25, 2009 · Viewed 12.2k times · Source

Why can't a computer program be proven just as a mathematical statement can? A mathematical proof is built up on other proofs, which are built up from yet more proofs and on down to axioms - those truths truths we hold as self evident.

Computer programs don't seem to have such a structure. If you write a computer program, how is it that you can take previous proven works and use them to show the truth of your program? You can't since none exist. Further, what are the axioms of programming? The very atomic truths of the field?

I don't have good answers to the above. But it seems software can't be proven because it is art and not science. How do you prove a Picasso?

Answer

A. Rex picture A. Rex · Jan 25, 2009

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.

Related questions

Subtracting a large unsigned binary number from a smaller one

I'm taking a computer organization and assembly language course. The written part of our lab this week has a question on it that has me stumped. The question reads... Subtract the following unsigned binary numbers (show the borrow and overflow …

Read More
Is the time complexity of the empty algorithm O(0)?

So given the following program: Is the time complexity of this program O(0)? In other words, is 0 O(0)? I thought answering this in a separate question would shed some light on this question. EDIT: Lots of good answers here! We …

Read More
Find the Simplified Sum of Products of a Boolean expression

Just having some problems with a simple simplification. I am doing a simplification for the majority decoder with 3 inputs A, B and C. Its output Y assumes 1 if 2 or all 3 inputs assume 1. Y assumes 0 otherwise. Select its correct switching function …

Read More