The person was talking about Rice's theorem [1], I believe. (It follows rather quickly from the unsolvability of the halting problem.) Proofs of program correctness might be exact for some programs, but Rice's theorem implies that you will never be able to come up with exact proofs for every program, and must rely on approximations. The entire field of program analysis and verification is dedicated to finding better approximations.

[1] https://secure.wikimedia.org/wikipedia/en/wiki/Rice%27s_theo...