I should rephrase that "every permutation of every instruction executed by the program". I'm not trying to prove that every program is correct, only that my program is correct. That is possible by using a well-defined and fully-proven subset of the available features of the language and processor.
For example, designing your program and CPU as a set of state machines allows you to define all possible states of the system (which are deliberately limited), define all the state transitions, then verify that every input condition for each state results in the correct state transition. Even if you simply brute force your way through every state and every transition instead of using mathematical generalizations, you've still proven that the program is correct.
As it turns out, this doesn't actually work. State derived program analysis has been shown to not be provable for all cases. Particularly when the state-space is very large, and when state transitions are non-atomic in the code, e.g. two or more state transitions in a code block.
The best research I've seen on this was done with Access Control Matrices in the Computer Security field. e.g. can you prove in a general sense that a sequence of atomic state changes to an ACM result in no violations of access control? The answer is, for atomic state changes you can prove that they are internally consistent, but not that they do not introduce a flaw in the ACM.
In other words, because proving software reduces to proving correctness, it only proves that the software is internally consistent. Basically it's a circular proof. It doesn't prove that the software is without flaw.
For example, designing your program and CPU as a set of state machines allows you to define all possible states of the system (which are deliberately limited), define all the state transitions, then verify that every input condition for each state results in the correct state transition. Even if you simply brute force your way through every state and every transition instead of using mathematical generalizations, you've still proven that the program is correct.