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 ...
- 274k
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 ...
- 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." (...
- 7,768
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
...
- 3,127
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 ...
- 274k
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 ...
- 704
40
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.♦
- 154k
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 ...
- 1,177
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 ...
- 13.3k
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 ...
- 309
16
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. ...
- 501
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 ...
- 38.5k
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.♦
- 154k
14
votes
How to prove greedy algorithm is correct
I will use the following simple sorting algorithm as an example:
...
- 5,931
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 ...
- 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 ...
- 22.1k
12
votes
Accepted
Why does this sort algorithm work?
It is a variant of bubble sort, however the endpoints of the array shift throughout the progress of the algorithm.
In particular it maintains the following invariant:
at the end of the $i$-th ...
- 20.6k
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 ...
- 219
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 ...
- 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.♦
- 154k
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 ...
- 274k
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 ...
- 8,308
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 - ...
- 12.3k
9
votes
Accepted
Matrix Chain Multiplication Greedy Approach
You don't state why you think that your algorithm is correct. In fact, it is incorrect. Here is an example. Consider the problem of computing the product of matrices of dimensions $2\times 1$, $1\...
- 274k
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 ...
- 29.6k
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$. ...
- 81.4k
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 ...
- 186
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....
- 274k
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 ...
- 81.4k
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 ...
- 38.5k
Only top scored, non community-wiki answers of a minimum length are eligible