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.