> 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.
I've actually done this a number of times before, but only in the ACM ICPC programming contest, so maybe a difference here is the environment in which people write programs vs proofs. In the contest, you have a team of three people and only one computer, and if you submit an incorrect solution, the only response you get back is "Wrong answer" with no detail about what test case was wrong. The typical way that teams approach this is to write code out completely on paper, then transcribe it from paper to the computer, run the provided test cases, and submit. Computer time is valuable, so if you run into a mistake that you can't figure out, it's common to print your code and look through the code on paper rather than trying to debug it on the computer.
When you train enough in an environment like that, you learn to be very careful about all of the details of the program you're writing. A single mistake can dramatically increase the time it takes to solve a problem, and there's pretty much no opportunity to "try it and see" like there is in normal programming. Also, the simple act of writing code down on paper and then copying it into the computer (double-checking as you go) gives you much more time to notice mistakes.
Mistakes are still common, of course, but I've had a number of times where I write out a program on paper, type it into the computer, compile it with no errors, run the sample test cases and have them all pass, and then submit it and and see that it's correct. I've never experienced something like that in any other programming environment, including other programming contests, which typically let you write your code on the computer.
Proofs tend to be the same type of environment: you write it out, with no compiler to help you, and you have plenty of time to read through it over and over before you have someone else check it for correctness. Maybe that sort of environment forces a level of care that you don't see as much in programming.
I've actually done this a number of times before, but only in the ACM ICPC programming contest, so maybe a difference here is the environment in which people write programs vs proofs. In the contest, you have a team of three people and only one computer, and if you submit an incorrect solution, the only response you get back is "Wrong answer" with no detail about what test case was wrong. The typical way that teams approach this is to write code out completely on paper, then transcribe it from paper to the computer, run the provided test cases, and submit. Computer time is valuable, so if you run into a mistake that you can't figure out, it's common to print your code and look through the code on paper rather than trying to debug it on the computer.
When you train enough in an environment like that, you learn to be very careful about all of the details of the program you're writing. A single mistake can dramatically increase the time it takes to solve a problem, and there's pretty much no opportunity to "try it and see" like there is in normal programming. Also, the simple act of writing code down on paper and then copying it into the computer (double-checking as you go) gives you much more time to notice mistakes.
Mistakes are still common, of course, but I've had a number of times where I write out a program on paper, type it into the computer, compile it with no errors, run the sample test cases and have them all pass, and then submit it and and see that it's correct. I've never experienced something like that in any other programming environment, including other programming contests, which typically let you write your code on the computer.
Proofs tend to be the same type of environment: you write it out, with no compiler to help you, and you have plenty of time to read through it over and over before you have someone else check it for correctness. Maybe that sort of environment forces a level of care that you don't see as much in programming.