However, these techniques are often too computationally expensive in many practical cases. Moreover, formal verification requires one to very precisely specify how a piece of code should behave, as well as how the environment in which it operates may behave. (Think of OS, network I/O, user interaction, etc.) This is another source of often prohibitive complexity.
Comments
You can mathematically prove whether a piece of code is 100% bug-free using formal verification techniques (https://en.wikipedia.org/wiki/Formal_verification).
However, these techniques are often too computationally expensive in many practical cases. Moreover, formal verification requires one to very precisely specify how a piece of code should behave, as well as how the environment in which it operates may behave. (Think of OS, network I/O, user interaction, etc.) This is another source of often prohibitive complexity.
And then you have the problem of proving that the specification is bug free...