This is spectacularly well stated:
Due to the unsolvability of the halting problem (and nearly any other question concerning program behaviour), no analysis that always terminates can be exact. Therefore we only have three alternatives:
- Consider systems with a finite number of finite behaviours (e.g. programs without loops) […]
- Ask interactively for help in case of doubt […]
- Accept approximate but correct information.
Neil D. Jones and Flemming Nielson, Abstract interpretation: a semantics-based tool for program analysis [PS]