Skip to main content
251 votes

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

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 ...
Yuval Filmus's user avatar
88 votes

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

(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 ...
Omar's user avatar
  • 1,136
64 votes

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

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." (...
Discrete lizard's user avatar
  • 8,303
53 votes

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

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 ...
Alexey Romanov's user avatar
43 votes

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

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 ...
Dan Bryant's user avatar
39 votes

Could Gödel’s incompleteness theorem be circumvented with a quine?

Here is the proof of Gödel's incompleteness theorem, in a nutshell, for a theory $T$. We construct a sentence $\Pi$ which states that "$T$ proves that $\Pi$ is false". The sentence mentions ...
Yuval Filmus's user avatar
31 votes

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

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 ...
user541686's user avatar
  • 1,167
26 votes

Could Gödel’s incompleteness theorem be circumvented with a quine?

Mainly because that proof would be part of mathematics too, and hence need proving itself. And that leads to an infinite loop in logic. No, that's not the flaw identified by Gödel’s incompleteness ...
Acccumulation's user avatar
25 votes

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

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 ...
Ariel's user avatar
  • 13.4k
20 votes

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

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 ...
Jeutnarg's user avatar
  • 309
13 votes

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

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 ...
Kaveh's user avatar
  • 22.3k
12 votes

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

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 ...
Readin's user avatar
  • 221
12 votes

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

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 ...
Fried Brice's user avatar
12 votes
Accepted

Is Coq synthetic or analytic?

The remark is about one specific usage of Coq, namely formalization of programming language theory. Let us first make clear the distinction between synthetic and analytic: In a synthetic approach to ...
Andrej Bauer's user avatar
  • 30.9k
12 votes

Could Gödel’s incompleteness theorem be circumvented with a quine?

[This is just my attempt to make Yuval Filmus's answer more mathematically accurate. Feel free to combine the answers, delete this one, or whatever seems best.] Here is the proof of Gödel's ...
Mike Spivey's user avatar
8 votes
Accepted

Is the Turing machine the only framework to analyse limits of computation?

Turing machines are far from being the only model of computation considered by computer scientists. Among well-studied models of computation are: Turing machines, λ-calculus (and its many variants, ...
Jean Abou Samra's user avatar
6 votes

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

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 ...
Félix Gagnon-Grenier's user avatar
5 votes

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

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 ...
Theodore Norvell's user avatar
5 votes

Using hypercomputation for "impossible" problems?

Nope. Russell's paradox and the liar's paradox aren't undecidable. They aren't even decision problems. As far as we know, hypercomputers don't exist. They are an imaginary idea that don't appear ...
D.W.'s user avatar
  • 162k
4 votes

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

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 ...
Ivan Kuckir's user avatar
4 votes

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

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 ...
Dan Brumleve's user avatar
4 votes

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

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 ...
wvxvw's user avatar
  • 1,388
4 votes

Why can humans solve certain "undecidable" problems?

As one of the comments notes, one should be aware that there are some pretty good algorithms for solving Higher Order Pattern Matching in practice (as a quick google search will reveal). I don't know ...
cody's user avatar
  • 8,233
4 votes

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

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 ...
navigator_'s user avatar
4 votes

Why has it taken so long to prove that P != NP?

Sometimes a short and easily verifiable proof takes a long time to discover. This may be due to several reasons. Maybe the general consensus in the research community is that the claim is probably not ...
Ilkka Törmä's user avatar
4 votes

Is P vs NP, a paradox in a hypothetical perspective?

This makes no sense to me. You imagine a scenario that is self-contradictory, and then observe that it is a contradiction, and.. then what? All that proves is that your scenario can't happen. It's ...
D.W.'s user avatar
  • 162k
3 votes

Why can humans solve certain "undecidable" problems?

Humans can solve some instances of undecidable problems and so can computers. Computers cannot solve all instances of undecidable problems, and not can humans.
gnasher729's user avatar
  • 30.6k
3 votes

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

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. ...
Oleg Lobachev's user avatar
3 votes

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

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 ...
user2138038's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible