Good point and great analogy, though I think EWD might be turning over in his grave. While the error detection built into compilers and the testing process are, in general, indispensable tools for developing stable software, a program that executes without any evidence of error is a great distance from a program that has been shown to be correct.
It's still easier to build up an understanding of computers under that environment. You may not be proving your programs correct, but you are probably proving them useful.
