"Would this be true even of formally proven code?" In functional languages functions are typically split into groups: pure and impure. The pure functions, in principle, can be formally proven to work correctly every time. The impure functions such as I/O or database queries can not be given such a guarantee because one can not guarantee inputs will be what you expect or accounted for. So even using a functional techniques at best only partially mitigates the problem. In imperative languages where the program state is much more mutable the problem is even worse (did one unintentionally change a more global variable for example).
The point being made is testing will not cover all the potential cases - they are often infinite - but only those that experience and judgement deems the most important.
Biting the hand that feeds IT
