# Tag Info

### 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 ...
• 278k

### 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 ...
• 1,136

### 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." (...
• 8,303

### 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 ...
• 3,192

### 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 ...
• 704

### 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 ...
• 278k

### 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 ...
• 1,167

### 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 ...

### 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 ...
• 13.4k

### 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 ...
• 309

### 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 ...
• 22.3k

### 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 ...
• 221

### 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 ...
• 219
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 ...
• 30.9k

### 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 ...
• 221
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, ...

### 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 ...

### 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 ...

### 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 ...
• 162k

### 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 ...
• 227

### 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 ...
• 169

### 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 ...
• 1,388

### 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 ...
• 8,233

### 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 ...
• 141

### 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 ...
• 288

### 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 ...
• 162k

### 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.
• 30.6k