Best way to "verify" programs [closed]

As we know, determining the semantic properties of programs is an undecidable problem (e.g. Halting, commonly attributed to Turing). But tools such as static analysis (notably that of Clang/LLVM) are developed nonetheless. In theoretical IT security (cryptography mostly), we have a class of tools known as "formal verification tools", where we can "prove" the soundness of "protocols" - these formal verification tools are developed from proof assistants from maths if I recall correctly. But they do no help when we implement a protocol in code, because codes can have all sorts of unexpected side channels that always can go amiss during design. If we can't have 100% confidence in the program we produce, then what're the closest "methodologies" we have for quality guarantee? (which I think means more than just "assurance")

May 17, 2025 - 14:14

As we know, determining the semantic properties of programs is an undecidable problem (e.g. Halting, commonly attributed to Turing). But tools such as static analysis (notably that of Clang/LLVM) are developed nonetheless.

In theoretical IT security (cryptography mostly), we have a class of tools known as "formal verification tools", where we can "prove" the soundness of "protocols" - these formal verification tools are developed from proof assistants from maths if I recall correctly. But they do no help when we implement a protocol in code, because codes can have all sorts of unexpected side channels that always can go amiss during design.

If we can't have 100% confidence in the program we produce, then what're the closest "methodologies" we have for quality guarantee? (which I think means more than just "assurance")