With enough effort, you can prove that your code conforms to the specification, but how do you prove that the specification conforms to your expectations?
You struggle to even do that. You can normally prove that some code conforms to a version of the specification that is explicitly formalised, but in practice, a large number of bugs are specification bugs and that will only increase the more you are forced to formalise the specification.
