I don't think this is really true either practically or theoretically. On the practical side, formally verifying program correctness is still very difficult for anything other than very simple programs. And on the theoretical side, some programs require arbitrarily difficult proofs to show that they satisfy even very simple specifications (e.g. consider a program to encode the fixpoint of the Collatz conjecture procedure, and our specification is that it always halts and returns 1).