Formal verification of arbitrary programs with arbitrary specifications will remain an unsolved problem (see halting problem). But formal verification of specific programs with specific specifications definitely is a solved problem.
As someone who came over from physics to CS this has always been one of the weirdest aspects of CS to me. That CS people believe that testing code (observing output) is sufficient to assume code correctness. You'd be laughed at in most hard sciences for doing this. I mean you can even ask the mathematicians, and there's a clear reason why proofs by contradiction are so powerful. But proof through empirical analysis is like saying "we haven't found a proof by contradiction, therefore it is true."
It seems that if this was true that formal verification should be performed much more frequently. No doubt would this be cheaper than hiring pen testers, paying out bug bounties, or incurring the costs of getting hacked (even more so getting unknowingly hacked). It also seems to reason that the NSA would have a pretty straight forward job: grab source code, run verification, exploit flaws, repeat the process as momentum is in your favor.
That should be easy to reason through even if you don't really know the formal verification process. We are constantly bombarded with evidence that testing isn't sufficient. This is why it's been so weird for me, because it's talked about in schooling and you can't program without running into this. So why has it been such a difficult lesson to learn?
The fact that a lot of code doesn't even have tests, and that a lot of people don't think even writing tests is a good thing, should shock you even more.
I teach so I'm not too shocked lol. But there's a big difference between beginners doing this and junior devs. But the amount of Sr devs doing this shit and not even understanding the limits of testing, well... a bit more shameful than surprising if you ask me
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).
