Why is writing mathematical proofs more fault-proof than writing code? (2011)

I think the line of reasoning is incorrect.

Most mathematical arguments are actually not formal, in the way a program is a formal language.

In many instances, there are not only ambiguities but errors in the mathematical expression. They only become formalised to an equivalent degree in a system like Isabelle or Coq.

Writing proofs in Isabelle and Coq is essentially the same process as writing highly functional code, and is susceptible to the same arduous process. It's hard because it's a formal language running on a rigid machine.

Programming would be easy if you specified everything in a semi --formal pseudo code, designed to be interpreted by a human mind that can fill in the blanks. This is what most mathematics is.

Because in mathematical proofs the preconditions are usually explicit and well understood. A program usually has reality-bound constraints that are not explicit, e.g. "does not work unless the target system has at least 3.5mb of memory" or "assumes that opcode X never fails" or "assumes memory is consistent and never is corrupted"

I consider myself a bit of an expert in this area, I work on lots of mathematical algorithms.

My experience is this isn't true. The reason it seems to be true is mathematicians will skip over writing out "boring" edge cases, which while hypothetically simple are often where the bugs occur in code.

Nice observation.

What really matters is the actual thinking about the actual subject. In nearly all math proofs, the writing is closer to that thinking than in coding. Or, each sentence in a math proof -- and well written proofs actually are written in sentences -- is closer to the thinking than for the programming language statements in the coding. Or, look at the statements in the coding -- without mnemonic identifier naming, they are close to just gibberish.

To get the coding closer to the thinking, that's the documentation in the coding. However the documentation is usually not as precise as the sentences in a math proof or the statements in code.

So, maybe we need to do something to get programming closer to the real thinking: For this, maybe try to have what we use in programming to be easier to describe. That is, in a math proof, we have numbers, sets, vectors, functions, etc. and at each point in the proof see clearly what these mean. In programming we have variables, arrays, structures, IF statements, loops, subroutines, and without documentation or careful reading don't see clearly what these mean.

Once I tried: I wrote some subroutines for sorting, permutations, etc. and tried to have clear properties for the operations the code die, properties that could reason about. Then for some uses of these subroutines, could do some logical reasoning much like in algebra in math. I didn't go very far with that idea!

> I've never heard of someone who wrote a big computer program with no mistakes in it in one go, and had full confidence that it would be bugless.

I've actually done this a number of times before, but only in the ACM ICPC programming contest, so maybe a difference here is the environment in which people write programs vs proofs. In the contest, you have a team of three people and only one computer, and if you submit an incorrect solution, the only response you get back is "Wrong answer" with no detail about what test case was wrong. The typical way that teams approach this is to write code out completely on paper, then transcribe it from paper to the computer, run the provided test cases, and submit. Computer time is valuable, so if you run into a mistake that you can't figure out, it's common to print your code and look through the code on paper rather than trying to debug it on the computer.

When you train enough in an environment like that, you learn to be very careful about all of the details of the program you're writing. A single mistake can dramatically increase the time it takes to solve a problem, and there's pretty much no opportunity to "try it and see" like there is in normal programming. Also, the simple act of writing code down on paper and then copying it into the computer (double-checking as you go) gives you much more time to notice mistakes.

Mistakes are still common, of course, but I've had a number of times where I write out a program on paper, type it into the computer, compile it with no errors, run the sample test cases and have them all pass, and then submit it and and see that it's correct. I've never experienced something like that in any other programming environment, including other programming contests, which typically let you write your code on the computer.

Proofs tend to be the same type of environment: you write it out, with no compiler to help you, and you have plenty of time to read through it over and over before you have someone else check it for correctness. Maybe that sort of environment forces a level of care that you don't see as much in programming.

The answer is simple.

In Mathematics you operate on a much higher level of concepts, and these concepts don't just fall out of thin air, but were sometimes decades or centuries in the making.

In programming though your concepts are made up very much on the fly (if you bother developing concepts at all; usually you just use your framework of choice and hope it got enough concepts baked in so you can survive), and therefore often not very good and coherent. That means you can not rely on them for any kind of correctness assessment.

I think it's not an apples to apples comparison.

In mathematics, there are abstract concepts like integers. For any i, i+1 is also an integer.

In programming, there is a MIN_INT and MAX_INT. If you write i/2, it's different than i/2.0. If you store a long string in a database, the column may be cut off at 32 chars because of the column type. Running string algorithms that sounds perfectly reasonable on ASCII may result in weird outcomes on Unicode. Most of these things also depend on the programming language, the compiler (MS, gnu, etc), the compiler version, OS, libraries, sometimes even the locale! A provably good crypto algorithm may be vulnerable to side-channel attacks. A mathematician may be happy to give an existential proof, but a programmer needs an implementation, and one that is polynomial [usually]. And so on...

The tldr is, the real world is more complicated, limited and nuanced than the abstract concepts of mathematics.

Compare writing a proof in Coq to writing a normal program. That is far more equal in terms of what you're doing. Writing a proof for people implicitly assumes a mountain of background information and interpolation between statements that doesn't exist in programming.

As the top voted answer says, proofs are at a very high level compared to programming.

Now imagine writing proofs on a very low level (check Metamath) where you work with wff and rewrite rules. It gets as tricky as programming.

I feel less confident of my proofs than my programs, because I can't run them, to see what happens. Yes, there are proof assistents like coq, but mathematicians look down on them.

Proofs are usually about some very small thing, and require a tremendous amount of work. Then, there is a huge literature for guidance and reusable elements (though, a lot of work to use it), and peer review to check it (also labour intensive).

I had experience both of writing programs and writing proofs including proofs in formally verified languages, e.g. Coq, Agda.

First of all, I think that the author underestimates the complexity of writing correct programs. What if integer overflow occurs? What is some exceptions happens somewhere? Programmers rarely consider all the pathological cases, while mathematicians must consider all of them. If program works most of the time, it's good enough for programmer but not good enough for mathematician.

Second, thanks to Curry Howard Correspondence, every formal proof has a corresponding program which 'constructs' a result of the theorem from preconditions, so, the proof is basically a program (and vice versa in a typed programming language).

In mathematical theorems the initial conditions are rather uniform without much if any of special cases. Thus mathematical proofs needs typically much less control flow to cover the initial conditions than computer programs. In fact many proofs are just straight deduction without single if to cover corner cases. Such type of "code" is simple to check. One just checks for logic of deduction, not the coverage of all initial conditions.

Adding to the arguments present here already, it's also often easier to work with mathematical formulas and concepts compared to programming concepts. For example:

pi. Easy in "math", effing hard to do in code. You don't have to worry about iee floats in "math". You don't have to worry about computational restrictions like ram, cpu time, null pointers etc.

Because in a program you can't have functions having their implementation left as an exercise for the computer. :^)

Both theorem proving and programming operate on an abstracted view of reallity ( in case of mathematics this reallity is often determined by some choice of axioms). By some metric the abstracted reallity of programming tends to be more complicated and noisy than that of mathematics.

One extra element I'd add is that what counts as an error in a proof is different than what counts as a bug. In pure math, an error is a strict failure of logic that breaks the proof. In programming, a bug doesn't need to only refer to something that stops the code from working. I've also heard it referred to as something that stops the code from working properly or efficiently, for instance. Mathematicians don't care about that because they have a different goal than a programmer, that is, to prove the truth of something (though some are motivated to produce more "elegant" proofs).

I don't agree that mathematical proofs are more fault-proof than code.

Mathematics is based more in the "spirit" of the idea and proof, rather than pedantically driving things down into the ultimate nuts and bolts. Many paper proofs are likely full of bugs deep in the details.

As intuitionism and machine formalism develop, and the standard of rigor rises, we might see entire branches of mathematics being relegated to the dustbin of historically interesting human endeavors but totally useless as foundations/formal assumptions for future work.

Two words, iteration and conditional execution.

Most math lacks these features common in programming.

With iteration you blend the results at time t with the results at time t+1.

Because of conditionals (if statements), a programming mistake at time t may not become evident till some much later step in the iteration, because the path through the logic is not guaranteed to be consistent.

Typically the data of all intervening steps has been lost by the time you encounter the error.

It was posted dec 11 2017, not dec 2011 :)

Most programming languages are unsound logic systems which allow us to prove true==false rather too easily!

If I spent as much time on a few lines of code as I spent in high school on a few lines of a proof, they'd be just as bug-proof.

Nobody is going to pay me to spend that kind of time on that little amount of code. Heck, I'm not even going to spend that kind of time on my own projects.

Because one is dealing with abstract theory with specific rules vs engineering in the real world.

One exists in the world of abstraction while the other lives in the real world.

Might as well ask why we can have a perfect circle in math while a perfect circle doesn't exist in the real world.

Because the interpreter for mathematical proofs is far more forgiving than the interpreter for code.

x = x + 1

I remember the fist time I saw that line and said, that's false. And it's been an ever ending divergence from pure math for the past 30 years.

Not sure if really related but I couldn't follow the math at school. For example in algebra the rules were complicated and required you to know things that are not explicitly set. Because of that I wrote my own functions to do what my teacher said. Then in the exams we are allowed to bring formulas, therefore I bring my own JavaScript function and I was the compiler :)

The teacher steps would resume in 5 sentences, but the function would be more long and include exceptions and weird cases. No room for mistakes with my JavaScript. No wonder I had the biggest score in the classroom.

I think the resounding answer has been over the years that written proofs aren't more fault proof, they're just better at hiding the faults because they lack explicitness. There has been a recent push for formal verification because it's easier to actually find issues with the proof.

Just peruse any upper level undergraduate math text. Flip to any proof and you’ll find “it follows naturally that...”

The bane of my existence as a math undergrad.

These days programming languages actually are used for expressing proofs. They can automatically check them to. For example the Coq theorem proving language.

https://en.wikipedia.org/wiki/Coq

Some would argue that writing code IS more fault proof than writing proofs the traditional way.

Because it's not true :-)

Writing mathematical proofs is as fault-proof as writing pseudo-code.

Writing machine-check proofs is as fault-proof as writing code.

I like the Lamport answer, implying that proofs are just as faulty as programs, they just don't get tested https://cs.stackexchange.com/a/85362/23759

One might say the amazing thing is that many (not all!) such theorems are correct, despite the errors. Somehow, mathematical insight sees the truth, despite formalism failure...

But, by this standard, most programs are "correct", they just have some inconsequential errors.

I think this goes to a systemic problem in mathematics, that proofs are not very rigorous. I've never found one convincing. Instead, math is slightly like English Literature, where you learn "theories" that are held to be true by the community. You get inducted, and off you go. It's not purely objective.

Of course, this doesn't explain the usefulness of mathematics when applied to reality, so I only claim it's "slightly like" an Arts subject. Perhaps some survivor bias, and engineers fix any problems.

Because we generally only accept mathematical proofs from highly-trained experts, and no one would hire the kid next door, who taught himself math and seems to spend a lot of time fooling around with calculators to do professional work in mathematics?

Depends on how you define fault here. Is it mere logical correctness of code or any error that might occur when code executes. If we follow former definition of fault then , they both are similar in being "fault-proof". If we follow later definition then execution environment of the program comes into play and it depends on a lot of variables and their complex interplay, that it becomes much harder to provide any formal guarantees of fault tolerance.

However there are execution environments, read RTOS that try to be fault tolerant. Also various virtual machines like JVM,CLR try to provide fault tolerance to varying degrees.

With maths, you're merely discovering something which already exists. Programming is more like you're creating something new.

You know all the preconditions and constraints ahead of time.

With real world applied software that is very rarely the case.

math resides in the land of abtractions(fantasy land) and actual code has to run on actual physical machines in the real world. In the real world you can't just state an axiom and fix bugs as math people have solved all their problems in the past 150 years.

Posted 11 Dec, 2017, not 2011.