252 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,128
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
45 votes
Accepted

Why is data in computer science considered to be discrete?

Answer why was the data considered to be a discrete mathematical entity rather than a continuous one This was not a choice; it is theoretically and practically impossible to represent continuous, ...
AnoE's user avatar
  • 1,273
45 votes
Accepted

Do any programming languages use general recursive functions as their basis?

Direct answer to the question: yes, there are esoteric and highly impractical PLs based on $\mu$-recursive functions (think Whitespace), but no practical programming language is based on $\mu$-...
xuq01's user avatar
  • 1,190
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
40 votes

What exactly is a logic?

Fundamentally, a logic consists of two things. Syntax is a set of rules that determine what is and is not a formula. Semantics is a set of rules that determine what formulae are "true" and what are "...
David Richerby'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
30 votes

Why is data in computer science considered to be discrete?

Computers represent a piece of data as a finite number of bits (zeros and ones) and the set of all finite bit strings is discrete. You can only work with, say, real numbers if you find some finite ...
Christian Matt's user avatar
26 votes

What exactly is a logic?

While fields such as computer science, mathematics and physics are relatively well-organized, Logic has a chaotic history. Its organization is really confusing so I think it's important to read some ...
Boris's user avatar
  • 493
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
Accepted

Mathematics topics or fields that increase computer programming proficiency?

So, there are many fields of math that are relevant to the Science of CS, but for programming specifically: Graph theory: this is the big one. Graphs and trees are everywhere. Networks, maps, paths ...
Joey Eremondi's user avatar
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
18 votes

What precisely differentiates Computer Science from Mathematics in theoretical context?

Theoretical computer science is what theoretical computer scientists do; and mathematics is what mathematicians do. Other than that, there is no accepted definition of either. One might argue that ...
Yuval Filmus's user avatar
18 votes

Shannon Entropy of 0.922, 3 Distinct Values

Here is a concrete encoding that can represent each symbol in less than 1 bit on average: First, split the input string into pairs of successive characters (e.g. AAAAAAAABC becomes AA|AA|AA|AA|BC). ...
nomadictype's user avatar
17 votes
Accepted

What is the role of mathematics in programming?

You don't need any math to write a Hello World or a very simple website. You will need to know some discrete mathematics and algorithm analysis to write a program that finds a route between two ...
svick's user avatar
  • 1,866
16 votes
Accepted

Shannon Entropy of 0.922, 3 Distinct Values

The entropy you've calculated isn't really for the specific string but, rather, for a random source of symbols that generates $A$ with probability $\tfrac{8}{10}$, and $B$ and $C$ with ...
David Richerby's user avatar
15 votes
Accepted

Monad in Haskell programming vs. Monad in category theory

A monad in Haskell is intended to be a monad on the category of types, when the category theory is done internally to the type theory. The capabilities of Haskell and similar languages are somewhat ...
Dan Doel's user avatar
  • 2,639
14 votes
Accepted

Predicate Logic Notation: What does a "dot" mean?

The dot just means "such that"; it's often omitted. The difference between the two formulas is the difference between "everybody has a mother" and "there is somebody who is everybody's mother."
David Richerby's user avatar
13 votes
Accepted

Mathematical conjectures equivalent to the halting of a Turing machine

Your question is answered by the arithmetical hierarchy. The existence of an odd perfect number is a $\Sigma_1$ statement, and so you can test it using a $\Sigma_1$ machine, which halts iff the ...
Yuval Filmus's user avatar
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.2k
13 votes

Shannon Entropy of 0.922, 3 Distinct Values

Let $\mathcal{D}$ be the following distribution over $\{A,B,C\}$: if $X \sim \mathcal{D}$ then $\Pr[X=A] = 4/5$ and $\Pr[X=B]=\Pr[X=C]=1/10$. For each $n$ we can construct prefix codes $C_n\colon \{A,...
Yuval Filmus's user avatar
13 votes
Accepted

How does a computer interpret real numbers?

They represent continuous quantities with discrete approximations. Mostly, this is done with floating point, which is analogous to scientific notation. Essentially, they work with something like $1....
David Richerby's user avatar
12 votes
Accepted

Minor Mistake in Computability, Complexity, and Languages?

There's no contradiction, here. The first case defines the partial function $g\colon \mathbb{N}\to\mathbb{N}$ given by $$g(n) = \begin{cases} x &\text{if $x\in\mathbb{N}$ and }x^2=n\\ \text{...
David Richerby's user avatar
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

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

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

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