math proofs are more robust than computer proofs

Via the ATS mailing list:

However, there is a huge difference between mathematical proofs and programs.

A mathematical proof is often very robust in the sense that mistakes in handling minor details can likely be remedied. A popular saying is that mathematical theorems are almost always true while mathematical proofs almost always contain mistakes. On the other hand, programs are not robust at all: a typo is all you need to crash a program. The very selling point of programming-with-theorem-proving as is supported in ATS is to facilitate the construction of correct programs by taking advantage of the inherent robustness of mathematical proofs: force your programs to go through rigorous typechecking while trusting your theorems (without proofs).

Math proofs are robust

Is this confusing constructing programs with running them?

Math proofs are robust because the *humans* playing with them are flexible in finding and correcting mistakes, while programs aren't robust because the *computers* playing with them are inflexible in finding and correcting mistakes.

The process of constructing *both* programs and proofs, on the other hand, may be made more robust by using computers' inflexibility to limit the damage caused by human flexibility (a.k.a. sloppiness). Assuming our math proof performing program is robust, of course.

Typos are an artifact of constructing our programs from text input.

By Sean Childs at Sat, 2011-11-12 02:36 | login or register to post comments

Who is confused?

The ATS post seems to be saying something that I don't suppose will generate much controversy. But it is talking about correctness as the fact that we haven't yet happened to notice any failure of a program to behave as expected, not about programs that have been proven correct, as this LtU topic title seems to suggest.

I do think that programs that seem to work and that have been proven correct against a comprehensible specification are generally going to be pretty robust. Especially if we have thought a bit about their operating environment.

By Charles Stewart at Mon, 2011-11-14 11:02 | login or register to post comments

Sure, that's what we get

Sure, that's what we get from the latter half of the quote.

The first half of that quote seems to imply something about correcting for errors (at run time) in a programs specification by the entity running the program.

I suppose if a program were to have such an ability, one of the things it would need is it's own internal language adequate for such a purpose.

By Sean Childs at Tue, 2011-11-15 23:39 | login or register to post comments

Programs and proofs differ

Programs and proofs differ in the dominant means used to debug them.

Programs are debugged largely by being run, which is an act of computation, hence fundamentally brittle. They can't be run on human wetware, because our wetware doesn't compute: it thinks. Computation and thought tend to use each other as metaphors because they're relatively more like each other than like anything else, but on an absolute scale they are very different; computers pretending to think are clumsy and inefficient, as are humans pretending to compute.

Proofs are (traditionally) debugged largely be being desk-checked, which is an act of thought. "Desk-checking" is what we call that activity when we do it to programs. The thing is, programs don't get nearly as thoroughly desk-checked as proofs. Part of that is that our programs are too big. Perhaps that's a failing of our programming technology — if we could build abstractions as fluently in our computational languages as we do in human languages, our programs might be vastly smaller. Also some part of it is that a lot of software is closed-source; that too cuts down on how much desk-checking is done. Given enough eyeballs, all bugs are shallow.

By John Shutt at Sat, 2011-11-12 05:33 | login or register to post comments

So where's P != NP proof?

If mistakes in mathematical proofs can be 'almost always' fixed, where is the P != NP proof?
I remember reading about several proofs for this, yet all these proofs had flaws, so where is the fixed version?

By renox at Mon, 2011-11-14 08:53 | login or register to post comments

There's proofs and proofs

I think we should interpret that as regarding proofs that the mathematical community has some confidence in.

Which is then not comparing like with like, since just what proportion of widely deployed software has the confidence of the community of people who worry about correctness?

By Charles Stewart at Mon, 2011-11-14 11:04 | login or register to post comments