The point of Turing's result and related theorems is not that you can't reason formally about programs, or understand or predict what they do, or prove that they are correct. It's that no automated method is powerful enough to decide nontrivial properties for every program; there are always programs for which the decision procedure will either say it doesn't know, or be wrong (or the decision procedure will take an infinite amount of time).
However, there are automated methods that can decide nontrivial properties for many programs, and the existence of programs where a given property can't be decided doesn't mean that the answers, when they exist, have to be wrong.
We do have specific programs in Turing-complete languages whose behavior or whose correctness to a specification is proven, and formal methods that can be applicable to them.
I think the article's conclusion might still be right, though: having environments where you can't always determine correctness may be playing with fire, so it may be a better choice to avoid that kind of risk entirely. But that doesn't mean that, given a program, we're always going to be completely in the dark about what the program does!