Quotes On Successful Software and Mathematics
(from Jim Larus, Microsoft Research)

What were the lessons I learned from so many years of intensive work on the practical problem of setting type by computer? One of the most important lessons, perhaps, is the fact that SOFTWARE IS HARD. From now on I shall have significantly greater respect for every successful software tool that I encounter. During the past decade I was surprised to learn that the writing of programs for TeX and Metafont proved to be much more difficult than all the other things I had done (like proving theorems or writing books). The creation of good software demands a significantly higher standard of accuracy than those other things do, and it requires a longer attention span than other intellectual tasks.

—Donald Knuth, Keynote address to 11th World Computer Congress (IFIP Congress 89).

I have spent a fair amount of effort during periods of my career exploring mathematical questions by computer. In view of that experience, I was astonished to see the statement of Jaffe and Quinn that mathematics is extremely slow and arduous, and that it is arguable the most disciplined of all human activities. The standard of correctness and completeness necessary to get a computer program to work at all is a couple of orders of magnitude higher than the mathematical communities standard of valid proofs. Nevertheless, large computer programs, even when they have been very carefully written and very carefully tested, always seem to have bugs.

When one considers how hard it is to write a computer program even approaching the intellectual scope of a good mathematics paper, and how much greater time and effort have to be put into it to make it 'almost' formally correct, it is preposterous to claim that mathematics as we practice it is anywhere near formally correct.

—William P. Thurston, “On Proof and Progress in Mathematics,” Bulletin of the American Mathematical Society, v. 30, n. 2, April 1994.