"The program, by definition, must be "correct" in order to execute"

This definition of 'correct' is why software may have a poor user interface and many security holes.

Your observation also assumes that the language is completely specified. In C, for example, certain constructs lead to undefined behavior. As a modification of the old warning, running your program may unexpectedly cause demons to fly out of your nose tomorrow. Execution therefore does not imply correctness.

Proof verification, btw, offer a "source of correction" for mathematics -https://en.wikipedia.org/wiki/Automated_theorem_proving#Rela... .