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?

Dunkin

@4thspace: Godel proved(!) that in any formal system of axioms there exists statements for which it is not possible to prove them true or false. You are making the assumption that all mathematics statements can be proven, which is unfortunately not the case. – Anachronous

@Mitch Wheat: Where is @4thspace assuming that all mathematical statements can be proven? – Mortgagor

Hope this question doesn't get closed, – Alimentary

The question is rather pesimistic, and its a not true assumption anyways – Ignominious

This question is gibberish. How do you prove a frog? How do you shave a sneeze? Please close. – Retool

Answer 1

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 (repaired 404 link is for seL4, see also the moved to location and the project's website).

Mortgagor

I've managed to go through my entire college career and the first couple of years of my professional career, and somehow I was never introduced to this awesome field. Thanks for the links, this is really interesting stuff! – Aardwolf

Answer 2

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.

Conroy

Are humans somehow magically immune to the halting problem? Of course you can automate proofs ... – Mortgagor

@A. Rex: If you design a program to halt, you can then prove if it does, indeed, halt. For arbitrary programs, not necessarily designed to halt, you cannot prove whether it does or does not halt. – Conroy

Indeed. I also can't prove arbitrary statements in number theory. But I do prove things in number theory, just not all of them. Why can't a program automatically prove some things, just like I can prove some things? You imply that you can "manually" do things but not "automatically" ... – Mortgagor

@A. Rex: You can -- easily -- automatically prove numerous trivial things. You can't prove loop halting automatically. That's what I'm saying. You can't automate one part of the proof system: halting. – Conroy

Let me just boil this down to one question: do you think that we, as humans, can prove something (perhaps the termination of loops) that computers fundamentally can't, because of the halting problem? – Mortgagor

@A Rex. Let me repeat my answer. Nothing can prove that an arbitrary program halts. Nothing. However, a human-designed program (when constrained in several ways) can be accompanied by a proof of halting. – Conroy

Okay, great, at least we're clear on that. All I was saying was anything that humans can do w.r.t. proving, computers can as well (in principle). We're absolutely in agreement that a proof of halting can't be obtained always, but definitely can be sometimes. – Mortgagor

Incidentally, I suppose +1 since that was the only part of your answer I didn't like ... but I still think it'd be good to make the distinction between "automate so that it always succeeds" and "automate so that it sometimes succeeds" clear. – Mortgagor

@A. Rex: "anything that humans can do w.r.t. proving, computers can as well (in principle)". Not true, actually. People have "intuition" which often reduce incredible search spaces down to a few quick tests. – Conroy

@A. Rex: "Do as well" is misleading, then. If you had said "do at all", I agree. "Do as well" I can't agree with. – Conroy

Sorry, "as well" meant "also". I definitely didn't mean anything related to good/well/etc. – Mortgagor

+1 for Dijkstra; -1 for silly computer != human debate in comments; +1 for coming to terms on terminology; -1 for wasting comment space; +1 for Dijkstra ;-) – Pigeonhole

I also don't see why humans would be fundamentally superior to computers when it comes to proving correctness. – Rositaroskes

@Wouter van Nifterick: Humans can design software to be proven -- some random algorithm is -- generally -- impossible to prove. And humans have better proof methods available than simple algorithms. Algorithms suffer from a limitation that no algorithm can prove loop termination. Humans simply are fundamentally superior at proof than an algorithm. – Conroy

+1 for Dijkstra and Gries. Both should be required reading in 1st and 2nd year of computing science degrees. – Quadrillion

@WoutervanNifterick But human minds (probably, in a sense) are algorithms. – Sorites

@Kyth'Py1k: Show conversation. My comment was from 6 years ago :) But yes.. brains are just algorithms indeed. Some people here seem to think that human brains have some magic or supernatural sparks that allow them to do things that computers can never do, and I don't share that view. There is no magic in our brains. Computers have the potential to do anything that we can do, but faster and more accurate. That includes coming up with clever proofs, or what we would call out-of-the-box thinking... – Rositaroskes

@Conroy But human minds (probably, in a sense) are algorithms. – Sorites

@WoutervanNifterick Oh, sorry Wouter. I meant to respond to S.Lott. – Sorites

Answer 3

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.

Delaine

Sure, you can create a provably correct program but the halting problem proves that there is no general solution for every program which is why "programs can't be proven". – Esophagus

nicerobot: You don't understand. "Programs can't be proven" in the same sense that "theorems can't be proven" -- it is not possible to prove them all. Many individual programs can be proven in the same way that many individual theorems can be proven. – Qintar

While you can prove in some cases that a program conforms to a specification, there is no way to prove that both 1) the specification is correct and 2) the method used to verify the specification is also correct. others have mentioned Godel, but Wittgenstein observed this phenomenon as well. – Chartism

Answer 4

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.

Harod

Answer 5

The halting problem only shows that there are programs that cannot be verified. A much more interesting and more practical question is what class of programs can be formally verified. Maybe every program anyone cares about could (in theory) be verified. In practice, so far, only very small programs have been proven correct.

Jolynjolynn

I'd suggest dropping "very" and leave it at "small". Some rather complex things have been proven very nicely. – Conroy

@Kim: interesting semi-comment. If the halting problem doesn't show that there is a class of programs that can't be proven to halt, what does it show? – Conroy

@Kim: The first sentence of John's answer is exactly what the halting problem shows. Maybe you were confused by the rest of his answer, which poses a different question? – Accouterment

It is not the case that every useful program can be verified. I have several times wanted programs that ended up being equivalent to HALT, or more ofter EQUIV (are these two programs equivalent) and obviously, those can't be verified. – Surgeon

Also, Kim isn't completely wrong. the halting problem proves that there are some programs that can't be WRITTEN. A universal verifier happens to be one of them. – Surgeon

Answer 6

If you're really interested in the topic, let me first recommend David Gries' "The Science of Programming", a classic introductory work on the topic.

It actually is possible to prove programs correct to some extent. You can write preconditions and postconditions and then prove that given a state that meets the preconditions, the resulting state after execution will meet the postconditions.

Where it gets tricky, however, is loops. For these, you additionally need to find a loop invariant and to show correct termination you need to find an upper bound function on the maximum possible number of iterations remaining after each loop. You also have to be able to show that this decreases by at least one after each iteration through the loop.

Once you have all this for a program, the proof is mechanical. But unfortunately, there's no way to automatically derive the invariant and bound functions for loops. Human intuition suffices for trivial cases with small loops, but realistically, complex programs quickly become intractable.

Benue

Answer 7

First, why are you saying "programs CAN'T be proven"?

What do you mean by "programs" anyway?

If by programs you're meaning algorithms don't you know Kruskal's? Dijkstra's? MST? Prim's? Binary Search? Mergesort? DP? All those things have mathematical models that describe their behaviors.

DESCRIBE. Math doesn't explain the why of things it simply draws a picture of the how. I can't prove to you that the Sun will rise tomorrow on the East but I can show the data where it has been doing that thing on the past.

You said: "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"

Wait? You CAN'T? http://en.wikipedia.org/wiki/Algorithm#Algorithmic_analysis

I can't show you "truth" I a program as much as I can't show you "truth" on language. Both are representations of our empirical understanding of the world. Not on "truth". Putting all gibberish aside I can demonstrate to you mathematically that a mergesort algorith will sort the elements on a list with O(nlogn) performance, that a Dijkstra will find the shortest path on a weighted graph, or that Euclid's algorithm will find you the greatest common divisor between two numbers. The "truth in my program" in that last case maybe that I'll find you the greatest common divisor between two numbers, don't you think?

With a recurrence equation I can delineate to you how your Fibonacci program works.

Now, is computer programming an art? I sure think it is. As much as mathematics.

Foreignborn

Good answer, if a bit too much hand-waving :D – Marimaria

Unfortunately, programs are more than algorithms. A very trivial non-terminating program can convince you of the distinction. – Ravish

Answer 8

I don't come from a mathematical background, so forgive my ignorance, but what does "to prove a program" mean? What are you proving? The correctness? The correctness is a specification that the program must verify to be "correct". But this specification is decided by a human, and how do you verify that this specification is correct?

To my mind, there are bugs in program because humans have difficulties expressing what they really want. alt text http://www.processdevelopers.com/images/PM_Build_Swing.gif

So what are you proving? Bugs caused by lack of attention?

Peart

Can't agree more. A little off-topic: I've seen this picture before, in the slides of a professor who lectures in implementing SAP in my college. – Roguish

That's a classic "bubble drawing" which was part of some dead boring project management courses I had to take.. I thought the question was about proving that some algorithm does what it should do and NOT arguing with a customer about features – Alkylation

@Nils, the question is about "program" to be proved, not algorithm. Trying to proove an algorithm is ok, because it is easy to express what we want the algorithm to do. But definitively, to proove a program is a non-sense to me – Peart

@NicolasDorier To prove a program is to prove it meets specification for all inputs. Specification can be made less subjective with contracts such as requires and ensures in c programming. – Hennahane

This is a comment, not an answer. – Retool

Answer 9

Further, what are the axioms of programming? The very atomic truths of the field?

I've TA'ed a course called Contract Based Programming (course homepage: http://www.daimi.au.dk/KBP2/). Here what I can extrapolate from the course (and other courses I've taken)

You have to formally (mathematically) define the semantics of your language. Let's think of a simple programming language; one that has global variables only, ints, int arrays, arithmetic, if-then-else, while, assignment and do-nothing [you can probably use a subset of any mainstream language as an "implementation" of this].

An execution state would be a list of pairs (variable name, value of variable). Read "{Q1} S1 {Q2}" as "executing statement S1 takes you from execution state Q1 to state Q2".

One axiom would then be "if both {Q1} S1 {Q2} and {Q2} S2 {Q3}, then {Q1} S1; S2 {Q3}". That is, if statement S1 takes you from state Q1 to Q2, and statement S2 takes you from Q2 to Q3, then "S1; S2" (S1 followed by S2) takes you from state Q1 to state Q3.

Another axiom would be "if {Q1 && e != 0} S1 {Q2} and {Q1 && e == 0} S2 {Q2}, then {Q1} if e then S1 else S2 {Q2}".

Now, a bit of refinement: the Qn's in {}'s would actually be statements about states, not states themselves.

Suppose that M(out, A1, A2) is a statement which does a merging of two sorted arrays and stores the result in out, and that all the words I use in the next example were expressed formally (mathematically). Then "{sorted(A1) && sorted(A2)} A := M(A1, A2) {sorted(A) && permutationOf(A, A1 concatened with A2)}" is the claim tha M correctly implements the merge algorithm.

One can try to prove this by using the above axioms (a few others would probably be needed. You're likely to need a loop, for one).

I hope this illustrates a bit of what proving programs correct might look like. And trust me: it takes a lot of work, even for seemingly simple algorithms, to prove them correct. I know, I read a lot of attempts ;-)

[if you read this: your hand-in was fine, it's all the other ones that caused me headaches ;-)]

Douse

Answer 10

Of course they can, as others have posted.

Proving a very small subroutine correct is a good exercise that IMHO every undergraduate in a programming-related degree program ought to be required to do. It gives you great insight into thinking about how to make your code clear, easily reviewable and maintainable.

However, in the real world it is of limited practical use.

First, just as programs have bugs, so do mathematical proofs. How do prove that a mathematical proof is really correct and doesn't have any errors? You can't. And for counter-example, any number of published mathematical proofs have had errors discovered in them, sometimes years later.

Second, you can't prove that a program is correct without having 'a priori' an unambiguous definition of what the program is supposed to do. But any unambiguous definition of what a program is supposed to do is a program. (Although it may be a program in some sort of specification language that you don't have a compiler for.) Therefore, before you can prove that a program is correct, you must first have another program that is equivalent and is known in advance to be correct. So QED the whole thing is futile.

I would recommend tracking down the classic "No Silver Bullet" article by Brooks.

Deceit

Answer 11

Not only can you prove programs, you can let your computer construct programs from proofs. See Coq. So you don't even have to worry about the possibility of having made a mistake in your implementation.

Aboveground

What you're saying is that there is a Coq specification compiler. How do you prove your Coq specification is correct? – Emetic

No, that wasn't what I said. While you have to give Coq a specification, that isn't sufficient. It also needs the constructive proof (which it can help you build) then it gives you a correct program. You have to provide the proof. You just don't have to translate it into a program, and risk errors. – Aboveground

Sounds like the days when Z was being talked about - providing a provably-correct program was actually the easy part, it was proving that that the builder was correct was hard – Hauge

Answer 12

Something that has not been mentioned here is the B - Method which is a formal method based system. It was used to develop the safety system of the Paris underground. There are tools available to support B and Event B development, notably Rodin.

Alimentary

#477459 mentions B, but I would leave your comment nonetheless, what with its mention of the Metro and Rodin. =) – Mortgagor

Answer 13

If you are looking for confidence, the alternative to proving programs is testing them. This is easier to understand and can be automated. It also allows for the class of programs for which proofs are mathematically not possible, as described above.

Above all, no proof is a substitute for passing acceptance tests:*

• Just because a program really does do what it says it does, doesn't mean it does what the user wants it to do.

  • Unless you can prove that what it says it does is what the user says they want.

    • Which you then have to prove is what they really want, because, being a user, they almost certainly don't know what they want. etc. Reductio ad absurdum.

*not to mention unit, coverage, functional, integration and all the other kinds of tests.

Hope this helps you on your path.

Eisenstein

Answer 14

They can. I spent many, many hours as a college freshman doing program correctness proofs.

The reason it's not practical on a macro scale is that writing a proof of a program tends to be a lot harder than writing the program. Also, programmers today tend to build systems, not write functions or programs.

On a micro scale, I sometimes do it mentally for individual functions, and tend to organize my code to make them easy to verify.

There's a famous article about the space shuttle software. They do proofs, or something equivalent. It's incredibly costly and time-consuming. That level of verification may be necessary for them, but for any kind of consumer or commercial software company, with current techniques, you'll get your lunch eaten by a competitor who delivers a 99.9% solution at 1% of the cost. Nobody's going to pay $5000 for an MS Office that's marginally more stable.

Hip

Answer 15

Theres much research in this area.. as others have said, the constructs within a program language are complex, and this only gets worse, when trying to validate or prove for any given inputs.

However, many languages allow for specifications, on what inputs are acceptable (preconditions), and also allow for specifying the end result (post conditions).

Such languages include: B, Event B, Ada, fortran.

And of course, there are many tools which are designed to help us prove certain properties about programs. For example, to prove deadlock freedom , one could crunch their program through SPIN.

There are also many tools out there that also help us detect logic errors. This can be done via static analysis (goanna, satabs) or actual execution of code (gnu valgrind?).

However, there is no one tool which really allows one to prove an entire program, from inception (specification), implementation and deployment. The B method comes close, but its implementation checking is very very weak. (It assumes that humans are infalible in the translation of speicficaiton into implmentation).

---

As a side note, when using the B method, you'll frequently find yourself building complex proofs from smaller axioms. (And the same applies for other exhasustive theorem provers).

Insignificance

Answer 16

Let us assume a purely functional language (ie Haskell). Side effects can be taken quite cleanly into account in such languages.

Proving that a program produces the right result requires you to specify:

1. a correspondance between data types and mathematical sets
2. a correspondance between Haskell functions and mathematical functions
3. a set of axioms specifying what functions you are allowed to build from others, and the corresponding contruction on the mathematical side.

This set of specifications is called denotational semantics. They allow you to prove the reason about programs using mathematics.

The good news is that the "structure of programs" (point 3 above) and the "structure of mathematical sets" are quite similar (the buzzword is topos, or cartesian closed category), so 1/ the proofs you do on the math side will easily be transferred into programmatic constructions 2/ the programs you write are easily shown to be mathematically correct.

Actinism

Answer 17

Your statement is wide so it's catching lots of fish.

The bottom line is: some programs can definitely be proven correct. All programs can not be proven correct.

Here's a trivial example which, mind you, is exactly the same kind of proof that destroyed set theory back in the day: make a program which can determine whether itself is correct, and if it finds that it is correct, give an incorrect answer.

This is Gödel's theorem, plain and simple.

But this is not so problematic, since we can prove many programs.

Smooth

Answer 18

Programs CAN be proven. It's quiet easy if you write them in language like for example Standard ML of New Jersey (SML/NJ).

Trahurn

Answer 19

Godel's Theorems notwithstanding...What would be the point? What simplistic "truths" would you like to prove? What would you want to derive from those truths? While I may eat these words...where's the practicality?

Monica

I would assume that the motivation is to prove that a program is correct, which would be quite useful. – Hartle

No...they do. But a software proof wouldn't have helped them...(AECL did not consider the design of the software during its assessment of how the machine might produce the desired results and what failure modes existed.) – Monica

The point stands nonetheless. If you're in a high-risk scenario (people dying, loss of billions of dollars), then a correctness proof would be nice. I presume this is one of the reasons NASA invests in verification research. – Mortgagor

If a program can be proven correct, then it can be proven to satisify all of the requirements listed in a requirements document. I would argue that many contractors would love to be able to do that. – Billbug

Requirements should be few and simple because their is no point to proove bad requirements. (the responsability to find this requirements are made by humans, this is error prone). – Peart

Answer 20

From a less abstract point fo view, proving something is a matter of reducing the field of uncertainty to a proven null set. That's wishful thinking because perfection just cannot be reached in the real world.

A computer program can be provably correct and fail in the real world if its environment are not (or cannot be) proven:

• the OS kernel, drivers and all user-mode libraries and concurrently executed programs must be proven, including their direct and indirect short-term and long-term side-effects,

• the hardware must always behave as expected (including with power-outages, water floods, earthquakes, EMF interferences, etc.),

• end-users must always behave as expected (the famous factor 'X').

Automatic error-correction is implemented in various hardware components (RAM, disks, controllers, etc.) but nevertheless hardware failures still happen - creating cascading errors and/or failures in... provably correct programs.

And I am not even trying to epilogue about end-user creativity...

So, a program (correctly) rated provably correct does not means that it is provably safe in the real-life.

It means that, for the set considered in a defined study (which can only be a subset of the real world), this program will behave as expected.

Unhappy

Answer 21

Just my 2 cents, adding to the interesting stuff already there.

Of all the programs that can't be proven, the most common ones are those performing IO (some unpredictible interaction with the world or the users). Even automated proofs sometimes just forget that "proven" programs" run on some physical hardware, not the ideal one described by the model.

On the other side mathematic proofs don't care much of the world. A recurring question with Maths is if it describes anything real. It is raised every time something new like imaginary numbers or non-euclidian space is invented. Then the question is forgotten as these new theories are such good tools. Like a good program, it just works.

Villegas

Answer 22

So much noise here, but I am going to shout in the wind anyhow...

"Prove correct" has different meanings in different contexts. In formal systems, "prove correct" means that a formula can be derived from other proven (or axiomatic) formulas. "Prove correct" in programming simply shows code to be equivalent to a formal specification. But how do you prove the formal spec correct? Sadly, there is no way to show a spec to be bug-free or a solution any real-world problem other than through testing.

Partan

Fred Brooks said it better: "Even perfect program verification can only establish that a program meets its specification. […] Much of the essence of building a program is in fact the debugging of the specification." – Anticlerical

Answer 23

Most answers focused on the practice and that's ok: in practice you don't care about formal proofing. But what's in theory?

Programs can be proven just as a mathematical statement can. But not in the sense you meant! In any sufficient powerful framework, there are mathematical statements (and programs) which cannot be proven! See here

Stogner

Answer 24

I haven't read all of the answers, but the way I see it, proving programs is pointless, that's why no one does it.

If you have a relatively small/medium project (say, 10K lines of code), then the proof is probably gonna be also 10k lines, if not longer.

Think about it, if the program can have bugs, the proof can also have "bugs". Maybe you'll need a proof for the proof!

Another thing to consider, programs are very very formal and precise. You can't get any more rigorous and formal, because the program code has to be executed by a very dumb machine.

While proofs are going to be read by humans, so they tend to be less rigorous than the actual code.

The only things you'll want to prove are low-level algorithms that operate on specific data structures (e.g. quicksort, insertion to a binary tree, etc).

These things are somewhat complicated, it's not immediately obvious why they work and/or whether they will always work. They're also basic building blocks for all other software.

Vespers

"While proofs are going to be read by humans, so they tend to be less rigorous than the actual code." -- unless they are machine-checkable proofs. – Pandit

How do you prove the correctness of the program that checks the proof? AND How do you prove that the proof actually proves the program in question and not something else? – Vespers

Answer 25

As others pointed out, (some) programs can indeed be proven.

One problem in practice however is that you first need something (i.e. an assumption or theorem) that you want to prove. So to prove something about a program you first need a formal description of what it should do (e.g. pre- and post-conditions).

In other words, you need a formal specification of the program. But getting even a reasonable (much less a rigorous formal) specification is already one of the hardest things in software development. Therefore it is generally very difficult to prove interesting things about a (real-world) program.

There are however some things which can be (and have been) more easily formalized (and proven). If you can at least prove that your program will not crash, that's already something :-).

BTW, some compiler warnings/errors are essentially (simple) proofs about a program. E.g., the Java compiler will prove that you never access an uninitialized variable in your code (otherwise it will give you a compiler error).

Allomerism

Answer 26

I read a bit about this, but there are two problems.

First, you can't prove some abstract thing called correctness. You can, if things are set up properly, prove that two formal systems are equivalent. You can prove that a program implements a set of specifications, and it's easiest to do this by constructing the proof and program more or less in parallel. Therefore, the specifications must be sufficiently detailed to provide something to prove against, and therefore the specification is effectively a program. The problem of writing a program to satisfy a purpose becomes the problem of writing a formal detailed specification of a program to satisfy a purpose, and that's not necessarily a step forward.

Second, programs are complicated. So are proofs of correctness. If you can make a mistake writing a program, you sure can make one proving. Dijkstra and Gries told me, essentially, that if I was a perfect mathematician I could be a good programmer. The value here is that proving and programming are two somewhat different thought processes, and at least in my experience I make different sorts of mistakes.

In my experience, proving programs isn't useless. When I am trying to do something I can describe formally, proving the implementation correct eliminates a whole lot of hard-to-find errors, primarily leaving the dumb ones, which I can catch easily in testing. On a project that must produce extremely bug-free code, it can be a useful adjunct. It isn't suitable for every application, and it's certainly no silver bullet.

Emetic

Answer 27

proving a program correct can only be done relative to the specification of the program; it is possible but expensive/time-consuming

some CASE systems produce programs more amenable to proofs than others - but again, this relies on a formal semantics of the specification...

...and so how do you prove the specification correct? Right! With more specifications!

Pigeonhole

Answer 28

If the program has a well defined objective and initial assumptions (ignoring Godel...) it can be proven. Find all primes,x, for 6<=x<=10, your answer is 7 and that can be proven. I wrote a program that plays NIM (the first Python program I ever wrote) and in theory the computer always wins after the game falls into a state in which the computer can win. I haven't been able to prove it as true, but it IS true (mathematically by a digital binary sum proof) I believe unless I made an error in the code. Did I make an error, no seriously, can someone tell me if this program is beatable?

There are some mathematical theorems that have been "proven" with computer code like the four color theorem. But there are objections, because like you said, can you prove the program?

Dull

Answer 29

Further, what are the axioms of programming? The very atomic truths of the field?

Are the opcodes the "atomic truths"? For example on seeing ...

mov ax,1

... mightn't a programmer assert as axiomatic that, barring a hardware problem, after executing this statement the CPU's ax register would now contain 1?

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?

The "previous work" then might be the run-time environment in which the new program runs.

The new program can be proven: apart from formal proofs, it can be proven "by inspection" and by various forms of "testing" (including "acceptance testing").

How do you prove a Picasso?

If software is more like industrial design or engineering than like art, a better question might be "how do you prove a bridge, or an airplane?"

Stout

Answer 30

Some parts of programs can be proved. For example, the C# compiler that statically verify and guarantee type safety, if the the compilation succeeds. But I suspect the core of your question is to prove that a program performs correctly. Many (I do not dare say most) algorithms can be proved to be correct, but a whole program probably cannot be proved statically due to the following:

• Verification requires all possible branches (calls, ifs and interupts) to be traversed, which in advanced program code has super-cubic time complexity (hence it will never complete within reasonable time).
• Some programming techniques, either through making components or using reflection, makes it impossible to statically predict execution of code (i.e. you don't know how another programmer will use your library, and the compiler has a hard time predict how reflection in a consumer will invoke functionality.

And those are just some...

Noeminoesis

Answer 31

Read up on the halting problem (which is about the difficulty of proving something as simple as whether a program completes or not). Fundamentally the problem is related to Gödel's incompleteness theorem.

Samaria

By this logic, we wouldn't do number theory. But I do, other people do, and computers do as well. – Mortgagor

Sure, en.wikipedia.org/wiki/Prover9_theorem_prover can probably (automatically) prove sqrt(2) is irrational. I'll see if I can find a definite example. – Mortgagor

I don't have to go far to find examples of computers doing group theory: cs.unm.edu/~mccune/otter/otter-examples/auto – Mortgagor

The MIZAR project is another decent example of automated number theory -- though it is more useful as a proof verifier. – Harod

OK fair comments. Just because there exist things which can't be proven doesn't mean every case is indeterminate. I should know this; I used to work in microelectronics and we had a formal methods team who did a great job finding broken state machines and potential deadlocks. – Samaria