Knuth is famous for the remark "Beware of bugs in the above code; I have only proved it correct, not tried it", and the implicit statement that a proof-of-correctness is not adequate to ensure that code will operate correctly is one I absolutely agree with
My boss told me a similar story of a computer science professor giving a cross-group talk in which he pitched the concept of formal methods to a group of physicists who, among other things, programmed collectors for particle experiments. (Supposedly this happened at Cornell in the seventies.) The CS professor enthusiastically and animatedly proved the correctness of an algorithm for solving a simple graph-coloring game and then asked whether there were any questions. One of the physicists raised his hand and asked, "How fast does it run?"
"That's the beauty of formal methods! Now that I've proved the algorithm correct, I already know it will produce the right answer. There are far too many possible inputs to verify correctness via testing, so there's actually no point in running it at all."
The problem with writing secure code that works well is making sure that all inputs conform to your well-defined set... i.e. they are a subset of your well-defined set.
Compounding on this is the non-apparent dimensionality of your sets. A good example of this would be concurrency. If a function doesn't have an exclusive lock an an array of data it's going to manipulate, the set could actually have two dimensions (one being time), in which the array could change.
I got a C- in Analysis II. I needed a C to get a Math minor, but decided it wasn't worth it.
You can see that computer science is an applied science. A mathematics professor would have given a proof that such an algorithm exists or, more likely, that algorithms exist for solving several more general problems, and left it at that.
My boss told me a similar story of a computer science professor giving a cross-group talk in which he pitched the concept of formal methods to a group of physicists who, among other things, programmed collectors for particle experiments. (Supposedly this happened at Cornell in the seventies.) The CS professor enthusiastically and animatedly proved the correctness of an algorithm for solving a simple graph-coloring game and then asked whether there were any questions. One of the physicists raised his hand and asked, "How fast does it run?"
"That's the beauty of formal methods! Now that I've proved the algorithm correct, I already know it will produce the right answer. There are far too many possible inputs to verify correctness via testing, so there's actually no point in running it at all."