Those assertions are a long way off absolutely true!
The undecidability of Turing machines in general doesn't say you can't reason about any programs, as you seem to claim, it says there exists programs which have unverifiable behaviour.
(Although the proof provides unnatural examples, in practice simple recursive mathematical functions such as the Collatz conjecture will probably always be beyond automated analysis.)
Of course software that was not written with verification in mind can be verified correct, provided it doesn't contains things such as an interpreter or complex conditional recursion. There are static analysis tools for analysing programs in languages such as C++ which make use of ATPs (automated theorem provers). For example, most of zlib has been proven correct using Coq. Yes, verification of the entirety of complex programs is in general impossible, but parts of them can still be verified. It's the most common use of ATPs, and an active area of research!
The undecidability of Turing machines in general doesn't say you can't reason about any programs, as you seem to claim, it says there exists programs which have unverifiable behaviour.
(Although the proof provides unnatural examples, in practice simple recursive mathematical functions such as the Collatz conjecture will probably always be beyond automated analysis.)
Of course software that was not written with verification in mind can be verified correct, provided it doesn't contains things such as an interpreter or complex conditional recursion. There are static analysis tools for analysing programs in languages such as C++ which make use of ATPs (automated theorem provers). For example, most of zlib has been proven correct using Coq. Yes, verification of the entirety of complex programs is in general impossible, but parts of them can still be verified. It's the most common use of ATPs, and an active area of research!