"Can a program ever be proven correct? No. There may be some very trivial toy programs that under very special conditions can be proven "correct" -- that is, we can mathematically prove that they will never give an incorrect result.5 In the real world of programs, however, the answer is no. At first, one is tempted to believe that it is simply a question of combinatorics. That is, if one considers all the permutations of all the paths through any non-trivial piece of software, one quickly comes to the conclusion that exhaustively testing any piece of software is an impossible task. This is analogous to the NP Complete problem. But, in fact, it is even worse than that. It turns out that proving programs correct is equivalent to solving the Halting Problem. And we know from Turing's work that that is an impossible task."

Your link is filled with nonsense, including the conclusion you took away from it here. We're talking about proving properties of a particular program here, not an arbitrary one. Please don't link to that in public again. It's a really terrible article.

No they didn't. And proving correctness of software isn't the same as solving the halting problem. You're confusing formal verification and static analysis (that doesn't mean that the latter doesn't work). Please, google Curry-Howard Isomorphism and Rice's Theorem, will ya?