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]