Why can't programs be proven?

Question

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 1

LIke AXIOMS, there are library routines that do routine, mundane processes like Input, output, mathematical computations and calculations, etc.

From these, we build modules, APIS, and other libraries that do more complicated tasks and processes.

These are like theorems.

Finally these libraries can be used to develop entire software suites, which are comparable to multiple page proofs.

There is a parallel between the two.....