Why is writing down mathematical proofs more fault-proof than writing computer code?
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.
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.
correctness-proof mathematical-foundations philosophy
Gilles 'SO- stop being evil'
$\begingroup$ Are you aware of proofs of correctness for programs, both on paper and mechanized in theorem provers? Both ones exist and contradict your update. is true is that programming as commonly taught has little to do with programming with correctness proofs. $\endgroup$ – Blaisorblade Dec 11 '17 at 21:09
$\begingroup$ Reminds me of a Knuth quote, I think "Beware of the above code! I only proved it correct, I never tested it" $\endgroup$ – Hagen von Eitzen Dec 12 '17 at 1:52
$\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$ – Gilles 'SO- stop being evil' Dec 19 '17 at 22:38
$\begingroup$ Find me a hand written math proof that is 100 million lines long and has no "bugs", and I'll give you everything I own. $\endgroup$ – Davor Dec 20 '17 at 12:02
$\begingroup$ Functional programs can be much easier to write than proofs, however, as soon as state comes in ... the difficulty explodes... $\endgroup$ – aoeu256 Aug 28 '19 at 0:13
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.
$\begingroup$ Is it possible that in the future, proof assistants will be used to check both your code and proof? Maybe it is time to Learn you an Agda? (sorry...) $\endgroup$ – Alex Vong Dec 14 '17 at 15:29
$\begingroup$ @AlexVong One problem with that is that a writing a formal specification for non-trivial code (so that you can verify that the code actually fulfills the specification) is nigh impossible. For example, can you imagine how complicated a formal specification for a browser would be (including all user interaction, all supported file formats and protocols etc.)? $\endgroup$ – svick Dec 14 '17 at 16:15
$\begingroup$ @svick You're right, for user interaction, it is sometimes not even clear what should be the right behavior. So we should instead focus ourselves on something with a proper formal specification (e.g. proof, compiler). $\endgroup$ – Alex Vong Dec 14 '17 at 16:47
$\begingroup$ Just to get functional languages more exposure (Clojure in this case), although this is O(n*w) instead of O(n): (defn maximum-window [data w] (->> data (partition w 1) (map #(reduce + %)) (reduce max))). O(n) isn't difficult to implement but it wouldn't follow the pseudocode so nicely. $\endgroup$ – NikoNyrh Dec 14 '17 at 19:25
$\begingroup$ Indeed. That might also be an explanation for why many people would find coding in lower-level languages to be much more tedious and less fun than coding in high-level, abstract languages. Though that may also differ by person, of course (Some might even enjoy building very low-level hardware/electronic circuits more than writing software that run on them? Also, lower-level code can still be irreplaceable in many cases and writing it well can be a scarce skill/feat worthy of commendation on its own). $\endgroup$ – xji Jan 19 '18 at 15:15
(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
OmarOmar
$\begingroup$ The point about "code reuse" is quite apropos. Translating a long proof from Russian into English takes quite a lot of typing; but translating a large computer program from, let's say, C++ into Java, takes quite a lot of thinking. Also, resurrecting a 3000-year-old proof in Ancient Greek is just about as easy; resurrecting a 30-year-old program in PL/1 is just about as hard, or harder. $\endgroup$ – Quuxplusone Dec 13 '17 at 22:48
$\begingroup$ The Ancient Greek example also made me realize: Computer programmers use a ton of local slang and colloquialisms, such as (void*)1 and open('/dev/null'), which may not even be portable between different subcultures, let alone translatable into the destination language. (The reader just kinda has to grok their approximate semantics by dint of long experience.) I think mathematical proofs contain less of this kind of "slang." If a proof uses a word, its actual universal meaning is supposed to be deducible by the reader somehow. Computer programs don't even have universal meanings! $\endgroup$ – Quuxplusone Dec 13 '17 at 22:53
$\begingroup$ +1, because as a constructivist, the rampant presumption of an $\infty$ distinct from an arbitrarily large value drives me nuts. This rises from a value-level fallacy to a logical fallacy when mathematicians start talking about infinite series and then make arguments based on those series, effecting an error on-par with a hidden-$\frac{0}{0}$ fallacy. $\endgroup$ – Nat Dec 18 '17 at 6:11
$\begingroup$ @Nat can you elaborate? I don't get it. $\endgroup$ – Gregory Magarshak Jan 1 '18 at 14:21
$\begingroup$ @GregoryMagarshak This answer demonstrated a case in which assuming that infinity's valid in series construction leads to a fallacy, which I was describing as being like this hidden-$\frac{0}{0}$ fallacy (the "disguised" version lower in the Wikipedia section). A classical mathematician might say that the mistake was assuming that an infinite series converges, though a constructivist would describe the fallacy as being an unqualified presumption of infinity. $\endgroup$ – Nat Jan 1 '18 at 15:23
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.
Discrete lizard♦Discrete lizard
$\begingroup$ I am just a layman; what did Dijkstra really refer to by "programming"? $\endgroup$ – Ovi Dec 13 '17 at 5:09
$\begingroup$ @Ovi I'm not precisely sure, but the main difference is that he talks about (non-trivial) algorithmic problem solving more than 'general' programming tasks, i.e. he certainly isn't talking about some CRUD program that needs to connect some existing architectures or other components etc. More on Dijkstra's opinion of programming can be seen in this answer $\endgroup$ – Discrete lizard♦ Dec 13 '17 at 9:03
$\begingroup$ Upvote for quoting Dijkstra, but you chose the wrong place! He has written a lot about this problem in the first paragraphs of Structured Programming. I wouldn't want to alter your answer by submitting a different quote, but I would hope you'd look into adding more from that paper to your answer! $\endgroup$ – wvxvw Dec 14 '17 at 15:55
$\begingroup$ @Ovi my guess on your question is that programming in Dijkstra's time more often meant writing assembly code vs. the modern era of high-level languages. Similarly, I am reading the 1974 edition of Mythical Man-Month, the concepts are still current but the technical references are systems-level assembler or PL/I, much different from what most people think of as programming today $\endgroup$ – JimLohse Dec 18 '17 at 17:45
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.
Alexey RomanovAlexey Romanov
$\begingroup$ Same paper: "Anecdotal evidence suggests that as many as a third of all papers published in mathematical journals contain mistakes — not just minor errors, but incorrect theorems and proofs". Well, that was in 90's, but is it that different today? Probably those papers existing those days, still exists and everything piles up... So, I'm not totally convinced that mathematical proofs provided in papers contain less errors. $\endgroup$ – MarkokraM Dec 12 '17 at 13:00
$\begingroup$ Fascinating anecdote, but I'm not seeing that it directly answers or engages with the question. Would you like to edit your answer to more directly respond to the question that was asked? Are you arguing that mathematical proofs are just as faulty as writing computer code? Do you have further evidence for that that you can provide? An anecdote or two doesn't really demonstrate that, does it? $\endgroup$ – D.W.♦ Dec 12 '17 at 16:32
$\begingroup$ @D.W. Leslie told in his sincere answer that his collegue made an investigation with 51 proofs published on Math Reviews at that time. In his opinion it is more than anecdotal but not fit for strong evidence due to several facts. Case was more complicated because some errors on proofs occured because they used errorneous proofs prom previously published papers etc. Would be a great research topic but requires so much work. How to verify math proofs programmatically is still a huge question. Apps made for interactive proof assistance are in very early stages. At least the interface of them. $\endgroup$ – MarkokraM Dec 14 '17 at 6:22
$\begingroup$ @D.W. The anecdote or two demonstrates how a mathematical proof could appear "correct" but actually be unsound. To anyone who has both written a complex computer algorithm and done a mathematical proof, and tried to write a computer algorithm like a mathematical proof and then discovering how the high level "algorithm" is betrayed by many, many bugs in the details, the result is not surprising at all. $\endgroup$ – Yakk Dec 15 '17 at 21:08
$\begingroup$ @Yakk That is certainly true. You could get some credit of being logical and correct on your part, but some discredit of not being throughout with sources you were relying. Again, software programmers and mathematicians both face similar problem. How to become 100% sure everything is bullet proof and stays so? By tests or by formal verification? $\endgroup$ – MarkokraM Dec 15 '17 at 21:24
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.
Dan BryantDan Bryant
$\begingroup$ +1 for your last paragraph. While mathematical proofs are in principle built on top of one another, usually the basics are well-understood, the analog of computer libraries (though they also have bugs...), and the actual proof is not too long. In contrast, consumer software is long and complicated, and so has many more opportunities to fail. $\endgroup$ – Yuval Filmus Dec 11 '17 at 21:00
$\begingroup$ In practice, the other issue with consumer software is that the 'correct' behavior is often poorly defined up-front and so what used to be correct later becomes wrong. It would be like trying to write a proof only to find out that people have decided to change the axioms. You can fix that in notation, right? $\endgroup$ – Dan Bryant Dec 11 '17 at 21:07
$\begingroup$ @DanBryant That situation does happen in mathematics. In particular the definitions of terms shift over time and are often ambiguous even right as their used. Imre Lakatos' "Proofs and Refutations" describes this with the term "polygon". A similar thing has happened with "function" and to a lesser extent "integral". Even today, "category" is not unambiguous and proofs and theorems can fail depending on what precisely you mean. $\endgroup$ – Derek Elkins left SE Dec 12 '17 at 5:17
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.
$\begingroup$ Great answer! except that as a computer, I object to your use of the word "needlessly". ;) [Suppose this was just one step in a larger proof aiming to prove that -x is composite. The fact that this step is wrong when -x = 3 is highly relevant to the correctness of the completed proof!] $\endgroup$ – Quuxplusone Dec 13 '17 at 23:00
$\begingroup$ @Quuxplusone: =P $\endgroup$ – user541686 Dec 13 '17 at 23:13
$\begingroup$ Computers can use symbolic math and non-deterministic rewriting rules too, its just that the languages we use like C++ are all very very low level and based on ancient technology (C had fewer features than Algol 60, for example). The only exceptions are the proof/checking languages like Idris/Agda, Lisp with symbolic solvers and Mathematica. ja.wolframalpha.com/input/… $\endgroup$ – aoeu256 Aug 28 '19 at 0:32
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.
ArielAriel
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:
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.
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).
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.
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).
JeutnargJeutnarg
$\begingroup$ Might be worth mentioning that programming's equivalent of 'indempotency' is functional purity, which is recognised and supported in some languages like Haskell. $\endgroup$ – Pharap Dec 19 '17 at 8:34
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.
KavehKaveh
$\begingroup$ I'm actually not sure who is worse off between programmers and mathematicians at formally (i.e. in a machine-checked manner) formulating correctness specifications and proving code correct for, say, a 10KLOC or larger program. On the one hand, you are completely correct that most programmers don't have well-developed theorem proving skills. On the other hand, large formal proofs are like large programs and require essentially software engineering skills to manage. I'm completely confident any informal proof of correctness for such a program would have no hope of being right. $\endgroup$ – Derek Elkins left SE Dec 15 '17 at 11:48
$\begingroup$ Maybe. In any case and just to clarify, I am not taking about formal proofs in my answer, just informal proofs at the level we see say in algorithms papers. $\endgroup$ – Kaveh Dec 15 '17 at 13:56
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.
ReadinReadin
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.
Fried BriceFried Brice
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.
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:
Félix Gagnon-GrenierFélix Gagnon-Grenier
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.
invariant p*p <= x
invariant pp == p*p
decreases x-p*p
invariant (p+q)*(p+q) <= x
invariant q > 0
invariant qq == q*q
invariant pq == p*q
decreases x-(p+q)*(p+q)
assert (p+q)*(p+q) <= x and pp==p*p and pq==p*q and qq==q*q and q>0
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.
Theodore NorvellTheodore Norvell
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.
navigator_navigator_
$\begingroup$ You seem to have a narrow view of what math is and a far too expansive view of what "proving" a computer program entails. You don't need to prove the whole system correct to prove a program correct, you just need to prove that it is correct assuming the other components meet their specifications. If they don't, it's not your program's fault. On the other hand, if your program breaks because it depends on details that aren't part of the specification of those components, e.g. variations of implementations of IEEE754, then that is your fault. $\endgroup$ – Derek Elkins left SE Dec 12 '17 at 5:32
$\begingroup$ Fair comment. I likely am misusing some terminology as its not my academic background. Although I do feel that assuming that other components are flawless is not a wise thing to do, due to my previous comments. $\endgroup$ – navigator_ Dec 12 '17 at 19:47
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.
wvxvwwvxvw
$\begingroup$ What do you mean by "long mathematical proofs"? The proof of the graph minor theorem is quite long, but it is not really disputed by anybody. The Feit-Thompson theorem has quite a long proof, but was never really in limbo. How do you compare the lengths of proofs and programs? Number of words? Are there really no noticeable differences between proofs and programs when you compare proofs and programs of similar complexity (length)? $\endgroup$ – Yuval Filmus Dec 14 '17 at 18:34
$\begingroup$ @YuvalFilmus just like in the quote: ten pages of assertions is long for humans. How do I judge about the length of a program? Well, Dikstra offered a metric: the length of its text. I think that it may be too simplistic, but it is a good heuristic nevertheless. There are other, more interesting metrics, like, for example, cyclomatic complexity $\endgroup$ – wvxvw Dec 15 '17 at 10:38
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!
Dan BrumleveDan Brumleve
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.
Ben CrowellBen Crowell
$\begingroup$ Two years of college-level math doesn't mean two years of focused on writing proofs (or spending any time writing proofs). That said, my impression is that it is common for middle-/early high-school geometry classes to include proofs, so apparently we can expect even 13 year olds to be able to write simple proofs with less than a school year of education on the topic. Step-by-step algebraic calculations are also essentially proofs. I think you are putting the bar for "trivial" for programming way too low and for proving way too high. $\endgroup$ – Derek Elkins left SE Dec 12 '17 at 5:41
$\begingroup$ We could write programs in the same way. You could imagine a requirement that every function/procedure you write has to provide a formal specification and a proof (in Coq, say) that it meets the spec. There are then ways to check that proof for correctness in a way that requires no judgement or understanding whatsoever. $\endgroup$ – D.W.♦ Dec 12 '17 at 16:47
$\begingroup$ @D.W.: You're assuming that (1) the desired behavior can be fully specified in all cases, (2) the necessary proof exists (i.e., the problem is not undecidable), and (3) if the proof exists, then we can find it. I think all three of these assumptions are false in at least some cases (probably almost all cases). Re 3, note that although some proofs may be easy, many proofs are very hard to find. $\endgroup$ – Ben Crowell Dec 13 '17 at 19:59
$\begingroup$ @DerekElkins: My claim that very few college students can write even trivial proofs is based on my own experience with my students. This is at a community college, so YMMV. The fact that some high school geometry classes include a heavy dose of proof-writing doesn't translate into the fact that all college students can write proofs. They are also supposed to know how to do basic algebra, but at my school roughly half of freshman calc students can't -- which helps to explain why so many fail. $\endgroup$ – Ben Crowell Dec 13 '17 at 20:02
$\begingroup$ That would be a good explanation to add to the answer, to explain why you can't take the same approach to check the program for correctness. Generally (2) and (3) are rarely an issue, either in practice or in principle (if you can't prove the program correct, write in a different way until you can prove it correct). However your (1) is an important point, and I think it would strengthen the answer to explain why that makes it hard to do the same thing for programs as we do for proofs. $\endgroup$ – D.W.♦ Dec 18 '17 at 3:54
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.
$\begingroup$ Wait, what makes you think mathematicians "fully understand" proofs and lemmas that they use? I'm not sure what difference between mathematicians and programmers you are trying to demonstrate here. $\endgroup$ – Derek Elkins left SE Dec 15 '17 at 11:53
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.
Oleg LobachevOleg Lobachev
$\begingroup$ I'm not totally seeing if this addresses the question. The OP did not make any indication the they were talking about programming languages with powerful type systems, and I think they mean more generic type systems. So Curry-Howard is kind of trivial in this case. $\endgroup$ – 6005 Dec 13 '17 at 1:17
$\begingroup$ I know it is a bit far-fetched for C or similar things. But my point is: math is closer than a typical CS beginner might think! $\endgroup$ – Oleg Lobachev Dec 13 '17 at 7:59
$\begingroup$ It seems you are a 'careless observer' of the Curry-Howards isomorphism, to which I referred in my answer. Even if we have an isomorphism between programs and proofs, it does not follow that the act of writing programs and writing proofs is similar at all. In fact, it may even be the case that all 'interesting' or 'typical' programs don't correspond to a typical proof and vice versa. $\endgroup$ – Discrete lizard♦ Dec 13 '17 at 17:28
$\begingroup$ @Discretelizard It's demonstrably not the case that "interesting" programs don't correspond to a "typical proof". Here's an example where I take someone's "typical proof" and produce a (sketch of) an undeniably interesting program (something closely related to Gaussian elimination). Equipped with suitably precise types, I think most "interesting" programs would be useful lemmas or theorems, but many (constructive) proofs have no real computational significance - they are just verifying side-conditions - though very many do. $\endgroup$ – Derek Elkins left SE Dec 15 '17 at 12:09
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$.
crobarcrobar
$\begingroup$ "Mathematical proofs operate on imaginary computing systems which have infinite memory and infinite computing power." Most mathematical proofs 'operate' on formal algebraic systems, e.g. the real numbers (where we have 'infinite precision'). This can also be done in programs: there are so-called computer algebra systems (CAS) that do precisely this! Furthermore, entire fields of mathematics are concerned with the fact that we cannot represent all real numbers exactly as finite floating point numbers. I think you are making a distinction between mathematics and programming where there is none. $\endgroup$ – Discrete lizard♦ Dec 13 '17 at 17:21
$\begingroup$ @Discretelizard, yes, special packages exist with arbitrary precision, but even then, available memory will limit the actual achievable precision. Also they are special packages. Only a tiny proportion of programming is done with such packages, and mostly in an academic setting. $\endgroup$ – crobar Dec 14 '17 at 10:24
$\begingroup$ I'm not talking about reaching arbitrary precision, but 'algebraic' precision: a CAS can reason about $\pi$ without approximating it, just like a human can. The algebraic representation of a number isn't really limited by memory. (and I think the computer beats the human when we consider memory limits.) Nevertheless, I do agree that a mathematical proof differs from a computer program in the sense that a machine sets tricky rules we have to obey. (compare with mathematics, where we set our own rules) I only think that the specific example you chose to show this isn't a very good one. $\endgroup$ – Discrete lizard♦ Dec 14 '17 at 10:52
$\begingroup$ @Discretelizard, I think my point still stands, most programmers are not using such CAS systems. They're far too slow for real-world programming. Most programming fundamentally involves operations on limited precision numbers. Top languages are C, C++, Python, Java etc. none use CAS style representation by default (although packages to do this might be created in them). Your counterexample is a tiny niche subset of computer languages/systems. $\endgroup$ – crobar Dec 14 '17 at 15:35
$\begingroup$ @crobar The issue with your answer is that the vast majority of detected bugs are not due to floating point errors or integer overflows (though those do contribute a decent number, and those aspects definitely make full correctness of a program much more unlikely). You could, however, make the more generic claim that mathematicians lack many of the concerns of programmers such as performance, time-to-market, maintainability, and a limited ability to change the requirements if they prove too challenging. $\endgroup$ – Derek Elkins left SE Dec 15 '17 at 12:40
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.
René AhnRené Ahn
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".
Ivan KuckirIvan Kuckir
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.
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.
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.
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.
James HollisJames Hollis
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.
Vladimir SotirovVladimir Sotirov
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.
supercatsupercat
$\begingroup$ "Only a small portion of mathematical statements which are true can be practically proven." - How are you measuring "portion"? Is this under some probability distribution? Do you have evidence to support this statement? $\endgroup$ – D.W.♦ Dec 12 '17 at 16:35
$\begingroup$ "computers are often called upon to do things beyond the range of what provably-correct software can accomplish." - Do you have any evidence for this? Do you have an example? Are you claiming "beyond what can in principle be proven correct" or "beyond what we can reasonably imagine proving in practice"? $\endgroup$ – D.W.♦ Dec 12 '17 at 16:36
$\begingroup$ @D.W.: If X and Y are orthogonal statements that are true but non-provable, then for every provable statement P, there will be at least two orthogonal statements (P and X), and (P and Y) which are true but non-provable. When dealing with infinite sets, such logic doesn't necessarily prove anything, since one could use similar logic to show that there are twice as many even integers as odd integers, since for every odd integer one can identify two even integers (4x) and (4x+2) that aren't associated with any other odd integers, but of course even and odd integers have equal cardinality. $\endgroup$ – supercat Dec 12 '17 at 18:14
$\begingroup$ @D.W.: The phrase "small portion" may thus only really make sense in describing the fraction of true statements which can be practically proven, but I think it's useful to understand that the inability to prove all true statements is not a "flaw". As for computers, many fields routinely use algorithms which have an extremely small, but non-zero, probability of failure, and then tune them so that probability is acceptably low (e.g. below that of the equipment being struck by a meteor). In many cases, various failure modes aren't independent, however, so it may be essentially impossible... $\endgroup$ – supercat Dec 12 '17 at 18:24
$\begingroup$ ...to determine the probabilities of different combinations of failures. If one estimates the probability of failure during an arbitrary one-minute period to be one in 10^-500, one could be off by hundreds of orders of magnitude and still have a reliable system, but if one is off by 494 orders of magnitude the system would fail about once every couple years. $\endgroup$ – supercat Dec 12 '17 at 18:28
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.
Arnab DattaArnab Datta
$\begingroup$ What is your definition of "fault" in a program then? $\endgroup$ – user56834 Dec 15 '17 at 10:45
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 )
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
ExeusExeus
$\begingroup$ "computer programs are waaay bigger than math proofs" That depends on the program and the proof. And much of this seems to be very speculative. $\endgroup$ – David Richerby Dec 21 '17 at 22:30
$\begingroup$ @DavidRicherby well I had on mind things like Last fermat's theorem and NASA's Apollo github.com/chrislgarry/Apollo-11 math.wisc.edu/~boston/869.pdf - and we aint even talking about operating systems and so on. $\endgroup$ – Exeus Dec 23 '17 at 9:11
Basic Levels:
Let's look at things at the simplest, and most basic level.
For math, we have:
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).
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.)
TOOGAMTOOGAM
$\begingroup$ While you make a nice case for the complexity of programming, you barely consider mathematics at all! In fact, you seem to underestimate the complexity involved in formal mathematics: "When you break things down in mathematics, you get to individual pieces that children can understand", really? Besides, the same could be said about sufficiently 'high-level' programming (e.g. Scratch is designed for children). Also note that Although the full C-spec isn't implementable, a compiler supporting an important subset has been shown formally correct using computer-assisted proofs. $\endgroup$ – Discrete lizard♦ Dec 21 '17 at 14:50
$\begingroup$ Agreed. In a research-level proof, you precisely won't see something on the level of $2+3=5$. Instead, you'll find statements like "can easily be proven by X", where X took you two years to master; or "is a straight-forward application of theorem Y", where Y took decades and dozens of people to prove. Of course, you can "compile" every research paper into elemenary, formal mathematics/logic -- finding myriads of bugs, I'm sure -- but nobody bothers to do so. (And not everybody agrees that that's good and well. So a few people do try to formalize mathematics.) $\endgroup$ – Raphael♦ Dec 21 '17 at 15:13
$\begingroup$ Meta note: if you are an expert in one thing and an expert beginner (or lower) in another, you are in the worst possible position to compare the two. $\endgroup$ – Raphael♦ Dec 21 '17 at 15:15
$\begingroup$ Discrete lizard - this is the Computer Science SE. Furthermore, having actually read other answers before I posted, I felt like they touched on mathematics much more than computers. I felt my answer was better by not making it longer just to add words that would largely be redundant with what was written elsewhere. /// As for Scratch, high level is more complex, not simpler (when looking at the perspective of fully understanding all moving parts). By this perspective, which I was writing from, Assembly is simpler than Scratch on top of other layers (with electronic NAND gates simpler yet) $\endgroup$ – TOOGAM Dec 22 '17 at 4:38
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.
Justin MeinersJustin Meiners
$\begingroup$ I'd say that mathematical proofs are fully capable of describing 'what' knowledge: take e.g. any proof that constructs an example to prove existence or a method to compute a value. Still, I agree that state is something absent in proofs, in the sense that there is no state other than that explicitly described by the author (or reader!). It is precisely this state that allows a program to do something the reader/author is unaware of, while this is impossible in a proof. (sure, proofs can have unintended features or results, but there is still some active thought required to get them) $\endgroup$ – Discrete lizard♦ Jan 20 '18 at 20:20
$\begingroup$ @Discretelizard This is a helpful comment. I think the line between the "what" and the "how to" is certainly fuzzy. Proving an algorithm does what you think it does, really isn't describing "how to" in my mind, its just guaranteeing certain properties hold. From a philosophical view, I think "how to" knowledge requires a correspondence with the world. Programs always do what you tell them. When you have a bug what you told it to do didn't correspond with the world (what you are modeling). Math, independent of an application (like physics problems) seems to be all dependent on coherence. $\endgroup$ – Justin Meiners Jan 20 '18 at 21:44
Not the answer you're looking for? Browse other questions tagged correctness-proof mathematical-foundations philosophy or ask your own question.
on "On the cruelty of really teaching computing science"
In this implementation of Hoare-partitioning Quicksort, why are additional checks for $i \leq j$ needed?
How to fool the "try some test cases" heuristic: Algorithms that appear correct, but are actually incorrect
Given the "programs as proofs" isomorphism, how do we know that the program isn't lying?
Proof Carrying LLVM?
Can we enumerate provably non-terminating functions?
Trying to understand this Quicksort Correctness proof
Proof of correctness of algorithm to determine whether the elements of an array are repeated an equal number of times
Can algorithm discovery be brute forced?
Proof for LeetCode: 11. Container With Most Water problem