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
51 votes

Example of an algorithm that lacks a proof of correctness

Here is an algorithm for the identity function: Input: $n$ Check if the $n$th binary string encodes a proof of $0 > 1$ in ZFC, and if so, output $n+1$ Otherwise, output $n$ Most people suspect ...
Yuval Filmus's user avatar
44 votes

How to prove greedy algorithm is correct

Ultimately, you'll need a mathematical proof of correctness. I'll get to some proof techniques for that below, but first, before diving into that, let me save you some time: before you look for a ...
D.W.'s user avatar
  • 162k
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
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
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
17 votes

How to fool the "try some test cases" heuristic: Algorithms that appear correct, but are actually incorrect

2D local maximum input: 2-dimensional $n \times n$ array $A$ output: a local maximum -- a pair $(i,j)$ such that $A[i,j]$ has no neighboring cell in the array that contains a strictly larger value. ...
Neal Young's user avatar
16 votes
Accepted

Can I use the following method to prove an algorithm is correct?

I am rather surprised that you raised this question since the meticulous and enlightening answers you have written to some math questions demonstrate sufficiently that you are capable of rigorous ...
John L.'s user avatar
  • 39.1k
15 votes

What are the flaws in this encryption algorithm?

This is not a secure encryption scheme. It is similar to a Hill cipher, and vulnerable to similar attacks. For instance, it is vulnerable to known-plaintext attacks: an attacker who observes a ...
D.W.'s user avatar
  • 162k
14 votes

How to prove greedy algorithm is correct

I will use the following simple sorting algorithm as an example: ...
adrianN's user avatar
  • 5,951
14 votes
Accepted

Trying to understand this Quicksort Correctness proof

We are indeed assuming $P(k)$ holds for all $k < n$. This is a generalization of the "From $P(n-1)$, we prove $P(n)$" style of proof you're familiar with. The proof you describe is known as the ...
Rick Decker's user avatar
  • 14.8k
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?

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
11 votes
Accepted

Proof of correctness of algorithm to determine whether the elements of an array are repeated an equal number of times

No, your algorithm doesn't work. Consider if the array A is A = [1 1 1 1 1 2 2 3 3 3 3 3 3]. Then the array B will be B = [5 5 5 5 5 2 2 6 6 6 6 6 6]. The sum of B will be 65, and the length of B ...
D.W.'s user avatar
  • 162k
10 votes

What are the flaws in this encryption algorithm?

Cryptosystems which are algebraic in nature are amenable to algebraic cryptanalysis. If you are trying to design a secure cryptosystem for actual use, there is one important maxim that you should ...
Yuval Filmus's user avatar
10 votes

Example of an algorithm that lacks a proof of correctness

Most algorithms have not been proven correct in Hoare logic. The main reason is that such correctness proofs are extremely expensive as of Jan 2017, probably by several orders of magnitude in ...
Martin Berger's user avatar
10 votes
Accepted

Correctness of FIPS 186-4 square test algorithm

This is more or less Newton's method applied to the function $f:x\to x^2 - C$. The algorithm finds $r = \left\lfloor \sqrt{C}\right\rfloor$ and check whether $r^2 = C$ or not. If we define $g(x) = x - ...
Nathaniel's user avatar
  • 15.8k
9 votes
Accepted

Why proving programs correctness doesn't have the same importance as algorithms analysis or the theory of computation in practice?

On the contrary, it's certainly important practice, and is a huge area of research! Perhaps a better question might be, "why is proving programs correct not common in practice, or not a main feature ...
Joey Eremondi's user avatar
8 votes
Accepted

What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic?

Condition $A$ is stronger than condition $B$ if $A$ implies $B$. That is, if $B$ holds in all situations in which $A$ holds. Conversely, if $A$ is stronger than $B$, then $B$ is weaker than $A$. ...
David Richerby's user avatar
7 votes
Accepted

Is the inverse of MST cycle property always true? Why?

If you want to test whether a specific edge belongs to some MST, you can use the following property. Claim. An edge $e$ belongs some MST if and only if for every $\epsilon > 0$, if we reduce the ...
Yuval Filmus's user avatar
7 votes

Trying to understand this Quicksort Correctness proof

This proof uses the principle of complete induction: Suppose that: Base case: $P(1)$ Step: For every $n > 1$, if $P(1),\ldots,P(n-1)$ hold (induction hypothesis) then $P(n)$ also holds....
Yuval Filmus's user avatar
7 votes
Accepted

Proof of correctness of A star search algorithm

Check the original paper which talks about its correctness - Hart, Peter E., Nils J. Nilsson, and Bertram Raphael. "A formal basis for the heuristic determination of minimum cost paths." Systems ...
Nitin's user avatar
  • 186
7 votes

How to select a binary tree node uniformly at random

The algorithm works just fine. Note that each node's size field tells you the total number of nodes in the subtree rooted at that node. Throughout this answer, I'm ...
David Richerby's user avatar
7 votes
Accepted

Existence / non-existence of a sequence with short longest increasing subsequence and decreasing subsequence?

The answer to the OP's question is, no if $N\le 7$ and yes otherwise. For given any positive integer $r$ and $s$, the celebrated Erdős–Szekeres theorem shows that for any sequence of distinct real ...
John L.'s user avatar
  • 39.1k
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

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