It is true of course that there is no automatic procedure which takes in an arbitrary program and decides if it has a desired input/output behavior. (Whether an input program has a given “semantic property” is undecidable.)

But that doesn’t mean that it is impossible to have all our programs be formally verified. For that, if we have a formal specification for what each should do… Well, I suppose it’s possible that some program we would want is possible to implement with the desired properties, but not possible to prove that it has those properties? It is possible to enumerate (program, proof) pairs though.