3 ms·

It is an absolute truth in the sense that it is true for all code that was not specifically written to be formally proven correct. So, given an arbitrary piece

• skydhash 2y ago
  It's not impossible to verify it, it's impossible to automatically verify it with another program. Other issues are the underlying abstract machine (which can have its own bugs) and the surrounding environment (you either need to assert or/and sanitize your inputs).
• versteegen 2y ago
  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!