Anyway, requirements, specifications and programs are just multiple representations of the same thing. Ideally, we would just state some requirements and they would execute.
So the requirements/specification/program complex exists Just Because. Humans decided they want that: for their amusement, for the sake of supporting some enterprise or solving a problem, or to try to sell to other humans.
The complex contains several different representations because that's what it takes to bridge the gap between stating the requirements and making the machine carry them out.
A proof is something internal to that complex: that the specification corresponds to the requirements, and that the program implements the specification.
If we had just one artifact: a specification that executes, then there would be no concept of proof any more.
There is only the question whether the specification that was expressed is the one that was intended in the mind. That equivalence is no more susceptible to proof than, say, the correspondence between the Ceasar salad that the waiter just put on your table (and which you clearly specified) and the idea of whether you actually wanted one, or did you mistakenly say "Ceasar salad" in spite of having wanted a soup.
Plus, there is the external question of whether a specification has unintended consequences. That basically amounts to "you say you want that, but maybe you should revise what you want because of these bad things".
"You say you want plaintext passwords to be stored for easier recovery, and that can certainly be implemented (provably correctly, too) but consider the following ramifications ..."