Why is writing down mathematical proofs more fault-proof than writing computer code?

Question

I have noticed that I find it far easier to write down mathematical proofs without making any mistakes, than to write down a computer program without bugs.

It seems that this is something more widespread than just my experience. Most people make software bugs all the time in their programming, and they have the compiler to tell them what the mistake is all the time. 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. (In fact, hardly any programs are bugless, even many highly debugged ones).

Yet people can write entire papers or books of mathematical proofs without any compiler ever giving them feedback that they made a mistake, and sometimes without even getting feedback from others.

Let me be clear. this is not to say that people don't make mistakes in mathematical proofs, but for even mildly experienced mathematicians, the mistakes are usually not that problematic, and can be solved without the help of some "external oracle" like a compiler pointing to your mistake.

In fact, if this wasn't the case, then mathematics would scarcely be possible it seems to me.

So this led me to ask the question: What is so different about writing faultless mathematical proofs and writing faultless computer code that makes it so that the former is so much more tractable than the latter?

One could say that it is simply the fact that people have the "external oracle" of a compiler pointing them to their mistakes that makes programmers lazy, preventing them from doing what's necessary to write code rigorously. This view would mean that if they didn't have a compiler, they would be able to be as faultless as mathematicians.

You might find this persuasive, but based on my experience programming and writing down mathematical proofs, it seems intuitively to me that this is really not explanation. There seems to be something more fundamentally different about the two endeavours.

My initial thought is, that what might be the difference, is that for a mathematician, a correct proof only requires every single logical step to be correct. If every step is correct, the entire proof is correct. On the other hand, for a program to be bugless, not only every line of code has to be correct, but its relation to every other line of code in the program has to work as well.

In other words, if step $X$ in a proof is correct, then making a mistake in step $Y$ will not mess up step $X$ ever. But if a line of code $X$ is correctly written down, then making a mistake in line $Y$ will influence the working of line $X$, so that whenever we write line $X$ we have to take into account its relation to all other lines. We can use encapsulation and all those things to kind of limit this, but it cannot be removed completely.

This means that the procedure for checking for errors in a mathematical proof is essentially linear in the number of proof-steps, but the procedure for checking for errors in computer code is essentially exponential in the number of lines of code.

What do you think?

Note: This question has a large number of answers that explore a large variety of facts and viewpoints. Before you answer, please read all of them and answer only if you have something new to add. Redundant answers, or answers that don't back up opinions with facts, may be deleted.

Answer 1

Let me offer one reason and one misconception as an answer to your question.

The main reason that it is easier to write (seemingly) correct mathematical proofs is that they are written at a very high level. Suppose that you could write a program like this:

function MaximumWindow(A, n, w):
    using a sliding window, calculate (in O(n)) the sums of all length-w windows
    return the maximum sum (be smart and use only O(1) memory)

It would be much harder to go wrong when programming this way, since the specification of the program is much more succinct than its implementation. Indeed, every programmer who tries to convert pseudocode to code, especially to efficient code, encounters this large chasm between the idea of an algorithm and its implementation details. Mathematical proofs concentrate more on the ideas and less on the detail.

The real counterpart of code for mathematical proofs is computer-aided proofs. These are much harder to develop than the usual textual proofs, and one often discovers various hidden corners which are "obvious" to the reader (who usually doesn't even notice them), but not so obvious to the computer. Also, since the computer can only fill in relatively small gaps at present, the proofs must be elaborated to such a level that a human reading them will miss the forest for the trees.

An important misconception is that mathematical proofs are often correct. In fact, this is probably rather optimistic. It is very hard to write complicated proofs without mistakes, and papers often contain errors. Perhaps the most celebrated recent cases are Wiles' first attempt at (a special case of) the modularity theorem (which implies Fermat's last theorem), and various gaps in the classification of finite simple groups, including some 1000+ pages on quasithin groups which were written 20 years after the classification was supposedly finished.

A mistake in a paper of Voevodsky made him doubt written proofs so much that he started developing homotopy type theory, a logical framework useful for developing homotopy theory formally, and henceforth used a computer to verify all his subsequent work (at least according to his own admission). While this is an extreme (and at present, impractical) position, it is still the case that when using a result, one ought to go over the proof and check whether it is correct. In my area there are a few papers which are known to be wrong but have never been retracted, whose status is relayed from mouth to ear among experts.

Answer 2

(I am probably risking a few downvotes here, as I have no time/interest to make this a proper answer, but I find the text quoted (and the rest of the article cited) below to be quite insightful, also considering they are written by a well-known mathematician. Perhaps I can improve the answer later.)

The idea, which I suppose isn't particularly distinct from the existing answer, is that a "proof" or argument communicates to a mathematical community, where the purpose is to convince them that the (tedious) details can be filled, in principle, to attain a fully specified formal proof -- without often doing so at all. One critical instance of this is that you can use existing theorems by simply stating them, but code re-use is much more challenging in general. Also consider minor "bugs", which may completely render a piece of code useless (e.g., it SEGFAULTs) but may leave a mathematical argument largely intact (that is, if the error can be contained without the argument collapsing).

The standard of correctness and completeness necessary to get a computer program to work at all is a couple of orders of magnitude higher than the mathematical community's standard of valid proofs. Nonetheless, large computer programs, even when they have been very carefully written and very carefully tested, always seem to have bugs. [...] Mathematics as we practice it is much more formally complete and precise than other sciences, but it is much less formally complete and precise for its content than computer programs. The difference has to do not just with the amount of effort: the kind of effort is qualitatively different. In large computer programs, a tremendous proportion of effort must be spent on myriad compatibility issues: making sure that all definitions are consistent, developing "good" data structures that have useful but not cumbersome generality, deciding on the "right" generality for functions, etc. The proportion of energy spent on the working part of a large program, as distinguished from the bookkeeping part, is surprisingly small. Because of compatibility issues that almost inevitably escalate out of hand because the "right" definitions change as generality and functionality are added, computer programs usually need to be rewritten frequently, often from scratch.

ON PROOF AND PROGRESS IN MATHEMATICS (pp. 9-10), by WILLIAM P. THURSTON https://arxiv.org/pdf/math/9404236.pdf

Answer 3

Allow me to start by quoting E. W. Dijkstra:

"Programming is one of the most difficult branches of applied mathematics; the poorer mathematicians had better remain pure mathematicians." (from EWD498)

Although what Dijkstra meant with `programming' differs quite a bit from the current usage, there is still some merit in this quote. The other answers have already mentioned that the level of abstraction in mathematics is allowed to be a lot higher than in programming, meaning we can ignore some tricky parts if we wish to do so.

However, I believe that this is merely a consequence of a more fundamental difference between a proof and a computer program, which is their purpose.

The main purpose of a mathematical proof is, among others, to convince oneself that a mathematical claim is correct and, perhaps even more important, achieving understanding. Therefore, you may choose to only work in the mathematical world, where everything is created such that understanding can be reached by design (although some students beg to differ...) This is precisely what Dijkstra meant with "pure mathematicians", those who (almost) only concern themselves with mathematical facts and understanding their properties.

So, you should not be surprised producing correct proofs is relatively fault-proof: it is the point of the entire "exercise". (Still, this doesn't mean mistakes don't or barely exist, to err is only human, they say)

Now, if we consider programming, what is our purpose? We do not really seek understanding, we want something that works. But when does something "work"? Something works when we have successfully created something that allows some strange machine to complete the task we want it to do and preferably pretty fast too.

This is, I believe, the fundamental difference, as it means that our goal cannot simply be stated as some theorem which our program "proves", we desire something in the real world (whatever that is), not some mathematical artifact. This means that we cannot purely theoretically achieve our goal (although Dijkstra would have you try it irregardless) as we must appease the machine, hope that we actually know which task we want it to do and also be aware of things none considered, yet happen somehow.

So, in the end, there is no other way around than to just try it and probably fail, fix, fail and try again until we are somewhat satisfied with the result.

---

Note that your hypothesis writing fault-less proofs is simpler than fault-less programs (which are in fact different statements as @Ariel points out) may be in fact wrong, as proofs are often constructed via trial and error at some level. Still, I hope that this sheds some light on the question that is implied: "What really is the difference between proving some theorem and writing a program?" (To which a careless observer of the Curry-Howard correspondence might say: "Nothing at all!")

---

As @wvxvw mentioned in the comments, the following paragraphs from 'notes on Structured Programming' (EWD249, page 21) is very relevant:

(...) A program is never a goal in itself; the purpose of a program is to evoke computations and the purpose of the computations is to establish a desired effect. Although the program is the final product made by the programmer, the possible computations evoked by it - the "making" of which is left to the machine! - are the true subject matter of his trade. For instance, whenever a programmer states that his program is correct, he really makes an assertion about the computations it may evoke.

(...) In a sense the making of a program is therefore more difficult than the making of a mathematical theory: both program and theory are structured, timeless objects. But while the mathematical theory makes sense as it stands, the program only makes sense via its execution.

Answer 4

Lamport provides some ground for disagreement on prevalence of errors in proofs in How to write a proof (pages 8-9):

Some twenty years ago, I decided to write a proof of the Schroeder-Bernstein theorem for an introductory mathematics class. The simplest proof I could find was in Kelley’s classic general topology text. Since Kelley was writing for a more sophisticated audience, I had to add a great deal of explanation to his half-page proof. I had written five pages when I realized that Kelley’s proof was wrong. Recently, I wanted to illustrate a lecture on my proof style with a convincing incorrect proof, so I turned to Kelley. I could find nothing wrong with his proof; it seemed obviously correct! Reading and rereading the proof convinced me that either my memory had failed, or else I was very stupid twenty years ago. Still, Kelley’s proof was short and would serve as a nice example, so I started rewriting it as a structured proof. Within minutes, I rediscovered the error.

... The style was first applied to proofs of ordinary theorems in a paper I wrote with Martin Abadi. He had already written conventional proofs—proofs that were good enough to convince us and, presumably, the referees. Rewriting the proofs in a structured style, we discovered that almost every one had serious mistakes, though the theorems were correct. Any hope that incorrect proofs might not lead to incorrect theorems was destroyed in our next collaboration. Time and again, we would make a conjecture and write a proof sketch on the blackboard—a sketch that could easily have been turned into a convincing conventional proof—only to discover, by trying to write a structured proof, that the conjecture was false. Since then, I have never believed a result without a careful, structured proof. My skepticism has helped avoid numerous errors.

Answer 5

One big difference is that programs typically are written to operate on inputs, whereas mathematical proofs generally start from a set of axioms and prior-known theorems. Sometimes you have to cover multiple corner cases to get a sufficiently general proof, but the cases and their resolution is explicitly enumerated and the scope of the result is implicitly constrained to the cases covered.

Compare this with a computer program, which has to provide 'correct' output for a range of possible inputs. It's rarely possible to enumerate all inputs and try them all. Worse yet, suppose the program interacts with a human being and allows their input to modify the functioning? Human beings are notoriously unpredictable and the number of possible inputs to a reasonably large program with human interaction grows at a prodigious rate. You need to try to foresee all the different ways a program might be used and try to make all those use cases either work or at least fail in a reasonable way, when failure is the only option. And that's assuming you even know how it's supposed to work in all those obscure corner cases.

Finally, a large program can't really be compared to a single proof, even a complex one. A large program is probably more akin to collecting and reviewing a small library of literature, some of which may have errors which you need to work around. For programs more on the scale of a single proof, which might be a small algorithm implementation, let's say, experienced software engineers can/do complete them without making mistakes, especially when using modern tools that prevent/resolve common trivial errors (like spelling mistakes) which are equivalent to early issues you'd resolve in proofreading.

Answer 6

They say the problem with computers is that they do exactly what you tell them.

I think this might be one of the many reasons.

Notice that, with a computer program, the writer (you) is smart but the reader (CPU) is dumb.
But with a mathematical proof, the writer (you) is smart and the reader (reviewer) is also smart.

This means you can never afford to get into a "well, you know what I mean" situation with a computer. It does exactly what you tell it, without knowing your intentions.

For example, let's say this is a step in some proof:

\begin{align*} \displaystyle\frac{x^2 + 4x + 3}{x+3} = \displaystyle\frac{(x+1)(x+3)}{x+3} = x+1 \end{align*}

If you tell a computer to evaluate $x^2+4x+3$ and then divide it by $x+3$, it will choke on your program when you let $x = -3$. But a mathematician would not get stuck on this point needlessly. He would realize that this is most likely irrelevant to the point you are trying to make, and that giving up and complaining about this minor issue will not help anybody. He'll get what you mean because he doesn't just follow you; he understands you. It's harder to fail when your reader is smart.

Answer 7

One issue that I think was not addressed in Yuval's answer, is that it seems you are comparing different animals.

Saying "the code is correct" is a semantic statement, you mean to say that the object described by your code satisfies certain properties, e.g. for every input $n$ it computes $n!$. This is indeed a hard task, and to answer it, one has to look beyond mere syntax. Your mathematical analogy for this is "is this proof correct", which is hardly fair, as the correct analogy should be "is this theorem true, and if so how can we prove it?". While the former is a syntactic statement which could be "easily" verified, the latter is much harder (its hardness can be formalized). Think about the most complicated code you have ever tried to come up with, and compare it to trying to prove Poincaré's conjecture (now theorem), this should give you different proportions.

Verifying semantic properties of programs is undecidable (Rice's theorem), and analogously, checking if a statement in first order predicate logic is true is also undecidable. The point is that there is no real difference in hardness from the way you are looking at the problems. On the other hand, we can reason about syntactic properties of programs (compilers), and this is analogous to the fact that we can verify proofs. Bugs (the code doesn't do what I want) are semantic, so you should compare them to their correct counterpart.

I will strengthen Yuval and say that entire fields grew with the motivation of writing mathematical proofs that can be written and verified in some formal system, so even the verification process is not at all trivial.

Answer 8

What is so different about writing faultless mathematical proofs and writing faultless computer code that makes it so that the former is so much more tractable than the latter?

I believe that the primary reasons are idempotency (gives the same results for the same inputs) and immutability (doesn't change).

What if a mathematical proof could give different results if it was read on a Tuesday or when the year advanced to 2000 from 1999? What if part of a mathematical proof was to go back a few pages, re-write a few lines, and then start again from that point?

I'm sure that such a proof would be nearly as prone to bugs as a normal segment of computer code.

I see other secondary factors as well:

1. Mathematicians are usually far more educated before attempting to write a significant/publishable proof. 1/4 of self-titled professional developers started coding less than 6 years ago (see SO survey 2017), but I assume most mathematicians have over a decade of formal math education.
2. Mathematical proofs are rarely held to the same level of scrutiny as computer code. A single typo can/will break a program, but dozens of typos may not be sufficient to destroy a proof's value (just its readability).
3. The devil's in the details, and computer code cannot skip details. Proofs are free to skip steps which are deemed simple/routine. There are some nice syntactic sugars available in modern languages, but these are hard-coded and quite limited in comparison.
4. Mathematics is older and has a more solid foundation/core. There certainly is a plethora of new and shiny subfields in math, but most of the core principles have been in use for decades. This leads to stability. On the other side, programmers still disagree on basic coding methodology (just ask about Agile development and its adoption rate).

Answer 9

I agree with what Yuval has written. But also have a much simpler answer: In practice softwares engineers typically don't even try to check for correctness of their programs, they simply don't, they typically don't even write down the conditions that define when the program is correct.

There are various reasons for it. One is that most software engineers don't have the skills to clearly formulate problems mathematically nor they know how to write correctness proofs.

Another one is that defining correctness conditions for a complex software system (specially a distributed one) is a very difficult and time consuming task. They are expected to have something that seems to work in matter of weeks.

Another reason is that the correctness of a program depends on many other systems written by others which again so not have clear semantics. There is a Hyrum's law that essentially says if your library/service has an observable behavior (not part of its contract) someone will eventually depend on it. That essentially means the idea of developing software in modular form with clear contracts like lemmas in mathematics does not work in practice. It gets worse in languages in which reflection is used. Even if a program is correct today it might break down tomorrow when someone does some trivial refactoring in one of its dependencies.

In practice what typically happens is that they have tests. Tests act as what is expected from the program. Everytime a new bug is found, they add tests to catch it. It works to some extend, but it is not a correctness proof.

When people don't have the skills to define correctness nor write correct programs nor expected to do so and doing so is rather difficult it is no surprise that softwares are not correct.

But note also that at the end in better places software engineering is done by code review. That is the author of a program has to convince at least one other person that the program works correctly. That is the point some informal high level arguments are made. But again typically nothing close to a clear rigorous definition of correctness or proof of correctness happens.

In mathematics people are focused on correctness. In software development there are many things that a programmer needs to care about and there are trade offs between them. Having a bug-free software or even a good definition of correctness (with requirements changing over time) is an ideal, but it has to be traded off against other factors and one of the most important among them is time spent on developing it by existing developers. So in practice in better places the goal and processes are mitigating the risk of bugs as much as feasible rather than making the software bug-free.

Answer 10

I like Yuval's answer, but I wanted to riff off of it for a bit. One reason you might find it easier to write Math proofs might boil down to how platonic Math ontology is. To see what I mean, consider the following:

• Functions in Math are pure (the entire result of calling a function is completely encapsulated in the return value, which is deterministic and computed completely from the input value).
• Math doesn't have mutation or reassignment (when you need to model such things, functions and sequences are used).
• Math is referentially transparent (e.g. no pointers, no notion of call-by-name vs call-by-value) and Mathematical objects have extensional equality semantics (if "two" things are the same in every observable way, then they are in fact the same thing).

While it's arguable whether or not the above restrictions makes writing a program easier, I think there's broad agreement that the above restrictions do make reasoning about a program easier. The main thing you do when writing a Math proof is reason about the proof you're currently writing (since, unlike in programming, you never have to duplicate effort in Math as abstractions are free), so it's generally worth it to insist on the above restrictions.

Answer 11

There are a lot of good answers already but there are still more reasons math and programming aren't the same.

1 Mathematical proofs tend to be much simpler than computer programs. Consider the first steps of a hypothetical proof:

Let a be an integer

Let b be an integer

Let c = a+b

So far the proof is fine. Let's turn that into the first steps of a similar program:

Let a=input();

Let b=input();

Let c = a+b;

We already have a myriad of problems. Assuming that the user really did enter an integer, we have to check the bounds. Is a greater than -32768 (or whatever the min int on your system is)? Is a less than 32767? Now we have to check the same thing for b. And because we've added a and b the program isn't correct unless a+b is greater than -32768 and less than 32767. That's 5 separate conditions a programmer has to worry about that a mathematician can ignore. Not only does the programmer have to worry about them, he has to figure out what to do when one of those conditions isn't met and write code to do whetever he has decided is the way to handle those conditions. Math is simple. Programming is hard.

2 The questioner doesn't say whether he's referring to compile-time errors or run-time errors, but programmers generally just don't care about compile-time errors. The compiler finds them and they're easy to fix. They're like typos. How often do people type several paragraphs without errors the first time?

3 Training. From a very young age we are taught to do math, and we face the consequences of minor mistakes over and over again. A trained mathematician had to start solving multi-step algebra problems usually in middle school and had to do dozens (or more) such problems every week for a year. A single dropped negative sign caused an entire problem to be wrong. After algebra the problems got longer and more difficult. Programmers, on the other hand, usually have far less formal training. Many are self-taught (at least initially) and didn't get formal training until university. Even at the university level, the programmers have to take quite a few math classes while the mathematicians probably took one or two programming classes. It should hardly be surprising the even programmers tend to have decent math skills while mathematicians find it difficult to get a program right.

Answer 12

Fundamental mathematical proofs does not amount to a real world application, designed to meet live humans needs.

Humans will change their desires, needs, and requirements on what is possibly a daily basis in the realm of computer programs.

What is so different about writing faultless mathematical proofs and writing faultless computer code that makes it so that the former is so much more tractable than the latter?

With as clear a requirement as a mathematical problem, a faultless program could be written. Proving that Dijkstra's algorithm can find the shortest path between two points on a graph is not the same as implementing a program that accepts arbitrary inputs and find the shortest points between any two points in it.

There are memory, performance, and hardware concerns to manage. I wish we could not think about those when writing algorithms, that we could use pure and functional constructs to manage this, but computer programs live in the "real" world of hardware whereas mathematical proof resides in... "theory".

---

Or, to be more succinct:

Answer 13

I can't find the reference, but I think Tony Hoare once said something along the following lines: The difference between a checking a program and checking a proof is that a proof can be checked two lines at a time.

In a word: locality.

Proofs are written so that they can be easily checked. Programs are written so that they can be executed. For this reason, programmers usually leave out information that would be useful to someone checking the program.

Consider this program, where x is read-only

    assume x >= 0
    p := 0 ;
    var pp := 0 ;
    while( x >= pp + 2*p + 1 ) 
    {
        var q := 1 ;
        var qq := q ;
        var pq := p ;
        while(  pp + 4*pq + 4*qq <= x )
        {
            q, pq, qq := 2*q, 2*pq, 4*qq ;
        }
        p, pp := p + q, pp + 2*pq + qq ;
    }
    assert  p*p <= x < (p+1)*(p+1)

It is easy to execute, but difficult to check.

But if I add back in the missing assertions, you can check the program locally by just checking that each sequence of assignments is correct with repect to its pre- and postconditions and that, for each loop, the postcondition of the loop is implied by the invariant and the negation of the loop guard.

    assume x >= 0
    p := 0 ;
    var pp := 0 ; 
    while( x >= pp + 2*p + 1 ) 
        invariant p*p <= x 
        invariant pp == p*p
        decreases x-p*p 
    {
        var q := 1 ;
        var qq := q ; 
        var pq := p ; 
        while(  pp + 4*pq + 4*qq <= x )
            invariant (p+q)*(p+q) <= x
            invariant q > 0 
            invariant qq == q*q 
            invariant pq == p*q 
            decreases x-(p+q)*(p+q)
        {
            q, pq, qq := 2*q, 2*pq, 4*qq ;
        }
        assert (p+q)*(p+q) <= x and pp==p*p and pq==p*q and qq==q*q and q>0
        p, pp := p + q, pp + 2*pq + qq ;
    }
    assert  p*p <= x < (p+1)*(p+1)

Coming back to the original question: Why is writing down mathematical proofs more fault-proof than writing computer code? Since proofs are designed to be easily checked by their readers, they are easily checked by their authors and thus alert authors tend not to make (or at least keep) logical errors in their proofs. When we program, we often fail to write down the reason that our code is correct; the result is that it is hard for both the readers and the author of a program to check the code; the result is that authors make (and then keep) errors.

But there is hope. If, when we write a program, we also write down the reason that we think the program is correct, we can then check the code as we write it and thus write less buggy code. This also has the benefit that others can read our code and check it for themselves.

Answer 14

Looking at it from another angle, in a non-academic setting it often comes down to money.

As the other posts assert well, Math is a single abstract specification, therefore a proof needs to work consistently within just that specification to be proven. A computer program may operate on many implementations of the abstract specification of math - that is to say the way one language, or hardware manufacturer implements floating point mathematics may be slightly different than another which may cause slight fluctuations in results.

As such, 'proving' a computer program before writing it would then involve proving the logic at the hardware level, operating system level, driver level, programming language, compiler, maybe interpreter and so on, for every possible combination of hardware that the program could conceivably be run on and any conceivable data it may ingest. You'll probably find this level of preparation and understanding on space missions, weapons systems or nuclear power control systems, where failure means tens of billions of lost dollars and potentially many lost lives, but not much else.

For your 'everyday' programmer and/or business, it is far, far more cost effective to accept a certain level of accuracy in mostly-correct code and sell a usable product, and the developers may retroactively fix bugs as they are uncovered during its usage.

Answer 15

I think that your reasoning is valid, but your input is not. Mathematical proofs simply aren't more fault-tolerant than programs, if both are written by humans. Dijkstra was already quoted here, but I will offer an additional quote.

Yet we must organize the computations in such a way that our limited powers are sufficient to guarantee that the computation will establish the desired effect. This organizing includes the composition of the program and there we are faced with the next problem of size, viz. the length of the program text, and we should give this problem also explicit recognition. We should remain aware of the fact that the extent to which we can read or write a text is very much dependent on its size. [...]

It is in the same mood that I should like to draw the reader's attention to the fact that "clarity" has pronounced quantitative aspects, a fact many mathematicians, curiously enough, seem to be unaware of. A theorem stating the validity of a conclusion when ten pages full of conditions are satisfied is hardly a convenient tool, as all conditions have to be verified whenever the theorem is appealed to. In Euclidean geometry, Pythagoras' Theorem holds for any three points A, B and C such that through A and C a straight line can be drawn orthogonal to a straight line through B and C. How many mathematicians appreciate that the theorem remains applicable when some or all of the points A, B and C coincide? yet this seems largely responsible for the convenience with which Pythagoras Theorem can be used.

Summarizing: as a slow-witted human being I have a very small head and I had better learn to live with it and to respect my limitations and give them full credit, rather than to try to ignore them, for the latter vain effort will be punished by failure.

This is slightly edited last three paragraphs from first chapter of Dijkstra's Structured Programming.

To perhaps rephrase this, to apply better to your question: correctness is largely a function of size of your proof. Correctness of long mathematical proofs is very difficult to establish (lots of published "proofs" live in the limbo of uncertainty since nobody actually verified them). But, if you compare correctness of trivial programs to trivial proofs, there's likely no noticeable difference. However, automated proof assistants (in a broader sense, your Java compiler is also a proof assistant), let programs win by automating a lot of groundwork.

Answer 16

It's not. Mathematical proofs are exactly as buggy by nature, it's just that their readers are more permissive than a compiler. Similarly, the readers of a computer program are easily fooled into believing it is correct, at least until they try to run it.

For example, if we try to translate a mathematical proof into a formal language like ZFC, it will also contain bugs. That's because these proofs can get really long so we're forced to write a program to generate the proof. Few people go to the trouble, at their peril, although there is active research in formalizing foundational proofs.

And indeed, math can get BSOD! It wouldn't be the first time!

This orthodox idea that all mathematical proofs which have been sufficiently verified are essentially correct or can be made correct is the same one motivating your software project at work: as long as we stay on the roadmap, we'll get all the bugs out and the features complete — it's an iterative process leading to a definite final product.

Here's the flip side. Look, we've already got the funding, validated the business concept, all the documents are right here for you to read. We just need you to execute and it's a sure thing!

Let's not feel too sorry for Hilbert either, he knew what he was getting into. It's just business.

If you want to be really sure, take everything on a case-by-case basis and draw your own conclusions!

Answer 17

You should distinguish two different "categories":

• pseudo-proofs (or pseudo-code) - that is what you see in books. It is written in natural language (e.g. in English). That is what you should use to learn Math (or Algorithms).
• formal proofs (or formal code) - you write it when you need your proof (or code) to be mechanically verifiable (or executable). Such representation does not require any "human intelligence". It can be verified (or executed) mechanically, by following some predefined steps (usually done by computers today).

We have been using pseudo-code for thousands of years (e.g. Euclids algorithm). Writing formal code (in formal languages like C or Java) became extremely popular and useful after the invention of computers. But, sadly, formal proofs (in formal languages such as Principia Mathematica or Metamath) are not very popular. And since everybody writes pseudo-proofs today, people often argue about new proofs. Mistakes in them can be found years, decades or even centuries after the actual "proving".

Answer 18

We could ask whether it is more difficult in practice, or in principle, to write proofs or write code.

In practice, proving is much harder than coding. Very few people who have taken two years of college-level math can write proofs, even trivial ones. Among people who have taken two years of college-level CS, probably at least 30% can solve FizzBuzz.

But in principle, there are fundamental reasons why it's the other way around. Proofs can, at least in principle, be checked for correctness through a process that requires no judgment or understanding whatsoever. Programs can't -- we can't even tell, through any prescribed process, whether a program will halt.

Answer 19

As other answers have touched on in their answers(I want to elaborate), but a big part of the issue is library usage. Even with perfect documentation(as common as bugless code), it is impossible to transfer complete knowledge of a library to every programmer using the library. If the programmer doesn't perfectly understand their library, they may make mistakes when using it. Sometimes these may result in critical bugs that are discovered when the code doesn't work. But for minor bugs, these may go unnoticed.

A similar situation would be if a mathematician used existing proofs and lemmas without fully understanding them; their own proofs would likely be flawed. While this may suggest a solution is to perfectly learn every library one uses; this is practically very time consuming and may require domain knowledge the programmer doesn't have.(I know very little of DNA sequencing/protein synthesis; yet can work with these concepts using libraries).

More succinctly put, software engineering(engineering in general really) is based on encapsulating different levels of abstraction to allow people to focus on smaller areas of the problem they specialize in. This allows people to develop expertise in their area, but also requires excellent communication between each layer. When that communication isn't perfect, it causes problems.

Answer 20

I'll try to be original after all that great answers.

Programs are proofs

The Curry–Howard isomorphism tells us, the types in your program are the theorems and the actual code is their proof.

Admittedly, this is a very abstract and high-level view. The issue you, probably, mean, is that writing a typical code is harder because it gets too low-level. In most cases you "need to tell the machine what to do". Or, to look into this from other way round: mathematicians are really good at abstraction.

As a side note: "The music of streams" is one of the most beautiful bridges between both. It basically sets up things to be able to say "I want this in that way" and the machine magically does this exactly as desired.

Answer 21

None of the many other answers point out the following. Mathematical proofs operate on imaginary computing systems which have infinite memory and infinite computing power. They can therefore hold arbitrarily large numbers to infinite precision, and lose no precision in any calculation.

Real world computers fall somewhat short of this ideal meaning implementing algorithms on them requires more thought and work. Proofs can contain symbols which represent things which cannot be contained in a real-world computer's memory, e.g. $\pi$.

Answer 22

I see two important reasons why programs are more error prone than math proofs:

1: Programs contain variables or dynamic objects changing over time, whereas mathematical objects in proofs are normally static. Thus, notation in math can be used as direct support of reasoning, (and if a = b, this remains the case) where this does not work in programs. Also, this problem gets far worse where programs are parallel or have multiple threads.

2: Math often assumes relatively neatly defined objects (graphs, manifolds, rings, groups, etc.) whereas programming deals with very messy and rather irregular objects: finite precision arithmetic, finite stacks, character-integer conversions, pointers, garbage that needs collection , etc... The collection of conditions relevant to correctness is therefore very difficult to keep in mind.

Answer 23

1. Computer programs are tested in the real world. A tricky technical error in a long mathematical proof, that only a limited number of people can understand, has a good chance of remaining undetected. The same sort of error in a software product is likely to produce strange behavior that ordinary users notice. So the premise might not be correct.

2. Computer programs perform useful real world functions. They don't have to be 100% correct to do this, and high standards of correctness are pretty expensive. Proofs are only useful if they actually prove something, so skipping the '100% correct' part is not an option for mathematicians.

3. Mathematical proofs are clearly defined. If a proof is flawed, the author has made a mistake. Many bugs in computer programs occur because the requirements weren't properly communicated, or there is a compatibility issue with something the programmer has never heard of.

4. Many computer programs cannot be proven correct. They might solve informally defined problems like recognizing faces. Or they may be like stock market prediction software and have a formally defined goal but involve too many real world variables.

Answer 24

A large portion of mathematics as a human activity has been the developing of domain-specific languages in which verification of proofs is easy for a human to do.

A proof's quality is inversely proportional to its length and complexity. The length and complexity is often reduced by developing good notation for describing the situation at hand about which we are making a statement, along with the auxiliary concepts interacting within the particular proof under consideration.

This is not an easy process, and most proofs witnessed by people removed from the forefront of research happen to be in mathematical fields (like algebra and analysis) that have had hundreds, if not thousands, of years during which the notation of that field has been refined to the point where the act of actually writing down the proofs feels like a breeze.

At the forefront of research though, particularly if you work on problems that are not in fields with well-established or well-developed notation, I would wager the difficulty of even a writing a correct proof approaches the difficulty of writing a correct program. This would be because you would also have to at the same time write the analog of a programming-language design, train your neural network to compile it correctly, try writing the proof in that, run out of memory, try to optimize the language, iterate your brain learning the language, write the proof again, etc.

To reiterate, I think that writing correct proofs can approach the difficulty of writing correct programs in certain areas of mathematics, but those areas are necessarily young and under-developed because the very notion of progress in mathematics is intimately tied up with the easy of proof verification.

Another way of phrasing the point I want to make is that both programming languages and mathematics are at the end of the day designed so that computer programs and proofs respectively are possible to compile. It's just that compiling a computer program is done in a computer and ensures syntactic correctness which has usually little to do with correctness of the program itself, while "compiling" a proof is done by a human and ensures syntactic correctness which is the same thing as correctness of the proof.

Answer 25

The domains of input vary greatly. Even in exotic cases, mathematical inputs are very rigorously defined so there is abundant clarity on what the inputs are. With computing the domain of inputs is so vast: a computer program can accept humble numbers (the simplest to verify) or touch input from a smart phone. The ever expanding appetite for digitisation, and by extension computability, implies continuously increasing complexity of software beyond the bounds of what can easily be verified. This need for digitisation strains our current abilities to 'keep up' leading to what we commonly refer to as 'bugs'.

Here's a quote from https://www.technologyreview.com/2002/07/01/40875/why-software-is-so-bad/ which illustrates this:

“The classic dilemma in software is that people continually want more and more and more stuff,” says Nathan Myhrvold, former chief technology officer of Microsoft. Unfortunately, he notes, the constant demand for novelty means that software is always “in the bleeding-edge phase,” when products are inherently less reliable. In 1983, he says, Microsoft Word had only 27,000 lines of code. “Trouble is, it didn’t do very much”-which customers today wouldn’t accept. If Microsoft had not kept pumping up Word with new features, the product would no longer exist.

Answer 26

Only a small portion of mathematical statements which are true can be practically proven. More significantly, it would be impossible to construct a non-trivial(*) set of mathematical axioms that would allow all true statements to be proven. If one only needed to write programs to do a tiny fraction of the things which could be done with computers, it would be possible to write provably-correct software, but computers are often called upon to do things beyond the range of what provably-correct software can accomplish.

(*) It's possible to define a set of axioms which would allow all true statements to be enumerated, and thus proven, but those aren't generally very interesting. While it's possible to formally categorize sets of axioms into those which are or not, relatively-speaking, non-trivial, the key point is that the provable existence of statements which are true but can't be proven is not a flaw in a set of axioms. Adding axioms to make any existing true-but-unprovable statements provable would cause other statements to become true but without them provable.

Answer 27

You are honestly comparing apples and oranges here. Fault-proof and bug-free aren't the same thing.

If a program compares the numbers 2 and 3 and it says that 2 is greater than 3, then it could be because of a buggy implementation:

# Buggy implementation
function is_a_greater_than_b(a,b):
  return b > a

The program is still fault free though. When comparing two numbers a and b, it will always be able to tell you if b is bigger than the a. It's just not what you (the programmer) were supposed to ask the computer to do.

Answer 28

a) Because computer programs are waaay bigger than math proofs

a.1) I believe that there's more people used during writting complex computer program than during writting math proof. It means that mistake margin is higher.

b) Because CEOs/Shareholders care more about money than fixing small bugs, meanwhile you (as developer) have to do your tasks to meet some requirements / deadlines / demos

c) Because you can be programmer without "deep" knowledge in comp sci, meanwhile it'd be hard to do in math ( I believe )

Additionally:

NASA:

This software is bug-free. It is perfect, as perfect as human beings have achieved. Consider these stats: the last three versions of the program -- each 420,000 lines long - had just one error each. The last 11 versions of this software had a total of 17 errors.

Take the upgrade of the software to permit the shuttle to navigate with Global Positioning Satellites, a change that involves just 1.5% of the program, or 6,366 lines of code. The specifications for that one change run 2,500 pages, a volume thicker than a phone book. The specifications for the current program fill 30 volumes and run 40,000 pages.

https://www.fastcompany.com/28121/they-write-right-stuff

Answer 29

Basic Levels:

Let's look at things at the simplest, and most basic level.

For math, we have:
2+3=5

I learned about that when I was very, very young. I can look at the most basic elements: two objects, and three objects. Great.

For computer programming, most people tend to use a high-level language. Some high-level languages can even "compile" into one of the lower high-level languages, like C. C can then be translated into Assembly language. Assembly language then gets converted into machine code. A lot of people think the complexity ends there, but it doesn't: Modern CPUs take the machine code as instructions, but then run "micro code" to actually execute those instructions.

This means that, at the most basic level (dealing with the simplest of structures), we are now dealing with micro-code, which is embedded in the hardware and which most programmers don't even use directly, nor update. In fact, not only do most programmers not touch micro code (0 levels higher than micro code), most programmers don't touch machine code (1 level higher than micro code), nor even Assembly (2 levels higher than micro code) (except, perhaps, for a bit of formal training during college). Most programmers will spend time only 3 or more levels higher.

Furthermore, if we look at Assembly (which is as low level as people typically get), each individual step is typically understandable by people who have been trained and have the resources to interpret that step. In this sense, Assembly is much simpler than a higher level language. However, Assembly is so simple that performing complex tasks, or even mediocre tasks, is very tedious. Upper-level languages free us from that.

In a law about "reverse engineering", a judge declared that even if code can theoretically be handled one byte at a time, modern programs involve millions of bytes, so some sorts of records (like copies of code) must be made just for such an effort to be feasible. (Therefore internal development wasn't considered a violation of the generalized "no making copies" rule of copyright law.) (I'm probably thinking of making unauthorized Sega Genesis cartridges, but may be thinking of something said during the Game Genie case.)

Modernization:

Do you run code meant for 286s? Or do you run 64-bit code?

Mathematics uses fundamentals that extend back for millennia. With computers, people typically consider investment in something two decades old to be uselessly wasteful of resources. That means Mathematics can be a lot more thoroughly tested.

Standards of Used Tools:

I was taught (by a friend who had more formal computer programming training than myself) that there is no such thing as a bug-free C compiler that meets the C specifications. This is because the C language basically assumes the possibility of using infinite memory for the purpose of a stack. Obviously, such an impossible requirement had to be deviated from when people tried to make usable compilers that worked with actual machines that are a bit more finite in nature.

In practice, I have found that with JScript in Windows Script Host, I've been able to accomplish a lot of good using objects. (I like the environment because the toolset needed to try new code is built into modern versions of Microsoft Windows.) When using this environment, I've found that sometimes there is no easily-findable documentation on how the object works. However, using the object is so beneficial, that I do so anyway. So what I'd do is write code, which may be buggy as a hornet's nest, and do so in a nicely sandboxed environment where I can see the effects, and learn about the object's behaviors while interacting with it.

In other cases, sometimes only after I've figured out how an object behaves, I've found that the object (bundled with the operating system) is buggy, and that it is a known issue that Microsoft has intentionally decided will not be fixed.

In such scenarios, do I rely on OpenBSD, created by masterful programmers that create new releases on-schedule, on a regular basis (twice a year), with a famous security record of "only two remote holes" in 10+ years? (Even they have errata patches for less severe issues.) No, by no means. I don't rely on such a product with such higher quality, because I'm working for a business that support businesses that supply people with machines that use Microsoft Windows, so that is what my code needs to work on.

Practicality/usability require that I work on the platforms that people find useful, and that is a platform which is famously bad for security (even though tremendous improvements have been made from the early days of the millennium which the same company's products were much worse).

Summary

There are numerous reasons why computer programming is more error prone, and that is accepted by the community of computer users. In fact, most code is written in environments which will not tolerate error-free efforts. (Some exceptions, such as developing security protocols, may receive a bit more effort in this regard.) Besides the commonly thought of reasons of businesses not wanting to invest more money, and miss artificial deadlines to make customers happy, there is the impact of the march of technology which simply states that if you spend too much time, you will be working on an obsolete platform because things do change significantly within a decade.

Offhand, I can recall being surprised at just how short some very useful and popular functions were, when I saw some source code for strlen and strcpy. For instance, strlen may have been something like "int strlen(char *x){char y=x;while ((y++));return (y-x)-1;}"

However, typical computer programs are much lengthier than that. Also, a lot of modern programming will use other code which may be less thoroughly tested, or even known to be buggy. Today's systems are much more elaborate than what can easily be thought through, except by hand-waving away a lot of the minutia as "details handled by lower levels".

This mandatory complexity, and the certainty of working with complex and even wrong systems, makes computer programming a lot hardware to verify than a lot of mathematics where things tend to boil down to a lot simpler levels.

When you break things down in mathematics, you get to individual pieces that children can understand. Most people trust math; at least basic arithmetic (or, at least, counting).

When you really break down computer programming to see what's happening under the hood, you end up with broken implementations of broken standards and code that is ultimately executed electronically, and that physical implementation is just one step below microcode which most university-trained computer scientists don't dare touch (if they are even aware of it).

I've spoken with some programmers who are in college or recent graduates who outright object to the notion that bug-free code can be written. They've written off the possibility, and though they acknowledge that some impressive examples (which I have been able to show) are some convincing arguments, they consider such samples to be unrepresentative rare flukes, and still dismiss the possibility of being able to count on having such higher standards. (A much, much different attitude than the much more trustable foundation we see in math.)

Answer 30

Mathematical proofs describe "what" knowledge and programs describe "how to" knowledge".

Writing programs is more complex because the programmer has to reason about all the different states that can arise, and how the program's behavior changes as a result. Proofs use formulaic or categorical reasoning to prove things about other definitions.

Most bugs are caused by processes entering into states that the programmer did not anticipate. In a program you usually have thousands or, in a large system, millions of possible variables which are not static data, but actually transform the way program executes. All of these interacting together create behaviors which are impossible anticipate, especially in a modern computer where there are layers of abstraction changing underneath you.

In a proof, there is no changing state. The definitions and objects of discussion are fixed. Proving does require thinking about the problem generally and considering a lot of cases, but those cases are fixed by definitions.