214
$\begingroup$

I have noticed that I find it far easier to write down mathematical proofs without making any mistakes, than to write down a computer program without bugs.

It seems that this is something more widespread than just my experience. Most people make software bugs all the time in their programming, and they have the compiler to tell them what the mistake is all the time. I've never heard of someone who wrote a big computer program with no mistakes in it in one go, and had full confidence that it would be bugless. (In fact, hardly any programs are bugless, even many highly debugged ones).

Yet people can write entire papers or books of mathematical proofs without any compiler ever giving them feedback that they made a mistake, and sometimes without even getting feedback from others.

Let me be clear. this is not to say that people don't make mistakes in mathematical proofs, but for even mildly experienced mathematicians, the mistakes are usually not that problematic, and can be solved without the help of some "external oracle" like a compiler pointing to your mistake.

In fact, if this wasn't the case, then mathematics would scarcely be possible it seems to me.

So this led me to ask the question: 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?

One could say that it is simply the fact that people have the "external oracle" of a compiler pointing them to their mistakes that makes programmers lazy, preventing them from doing what's necessary to write code rigorously. This view would mean that if they didn't have a compiler, they would be able to be as faultless as mathematicians.

You might find this persuasive, but based on my experience programming and writing down mathematical proofs, it seems intuitively to me that this is really not explanation. There seems to be something more fundamentally different about the two endeavours.

My initial thought is, that what might be the difference, is that for a mathematician, a correct proof only requires every single logical step to be correct. If every step is correct, the entire proof is correct. On the other hand, for a program to be bugless, not only every line of code has to be correct, but its relation to every other line of code in the program has to work as well.

In other words, if step $X$ in a proof is correct, then making a mistake in step $Y$ will not mess up step $X$ ever. But if a line of code $X$ is correctly written down, then making a mistake in line $Y$ will influence the working of line $X$, so that whenever we write line $X$ we have to take into account its relation to all other lines. We can use encapsulation and all those things to kind of limit this, but it cannot be removed completely.

This means that the procedure for checking for errors in a mathematical proof is essentially linear in the number of proof-steps, but the procedure for checking for errors in computer code is essentially exponential in the number of lines of code.

What do you think?

Note: This question has a large number of answers that explore a large variety of facts and viewpoints. Before you answer, please read all of them and answer only if you have something new to add. Redundant answers, or answers that don't back up opinions with facts, may be deleted.

$\endgroup$
5
  • 6
    $\begingroup$ Are you aware of proofs of correctness for programs, both on paper and mechanized in theorem provers? Both ones exist and contradict your update. is true is that programming as commonly taught has little to do with programming with correctness proofs. $\endgroup$ Dec 11 '17 at 21:09
  • 87
    $\begingroup$ Reminds me of a Knuth quote, I think "Beware of the above code! I only proved it correct, I never tested it" $\endgroup$ Dec 12 '17 at 1:52
  • $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$ Dec 19 '17 at 22:38
  • 9
    $\begingroup$ Find me a hand written math proof that is 100 million lines long and has no "bugs", and I'll give you everything I own. $\endgroup$
    – Davor
    Dec 20 '17 at 12:02
  • 2
    $\begingroup$ Functional programs can be much easier to write than proofs, however, as soon as state comes in ... the difficulty explodes... $\endgroup$
    – aoeu256
    Aug 28 '19 at 0:13

31 Answers 31

1
2
0
$\begingroup$

There is a discussion over at crypto.stackexchange:

https://crypto.stackexchange.com/questions/88582/does-schnorrs-2021-factoring-method-show-that-the-rsa-cryptosystem-is-not-secur

Basically, there is a proof that products of two large primes, as they are used in RSA, can be factored reasonably quickly. The proof is hard. There is no universal agreement on whether it is correct or not at this moment.

Now someone could implement a program following this proof, and try out if it can factor products of large primes quickly or not. This problem has the nice property that you can run the algorithm, it should succeed, and when it succeeds it is very easy to check that it found the correct solution.

So in the mathematical proof, it is possible that the proof is accepted even when it is completely wrong. And of course if it works in most but not all cases. The program doesn't have that luxury, if it doesn't work, it doesn't work. If it gets wrong results, that is easily found. That makes it easier to write mathematical proofs that seem correct because faults are harder to find. For mathematical proofs that are proven 100% correct vs. programs that are proven 100% correct, that's probably equally difficult.

$\endgroup$
1
2

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.