[carbonica]

If that's intuitive for you already (great!) consider one step further: Rice's Theorem. Rice's Theorem in layman's term is "all nontrivial properties of a program are undecidable in the general case". "Undecidable" is the difficulty class of the halting problem (there are actually harder problems!).

A couple accessible examples:

1. Constant Propagation - we know that we'll never detect all compile-time constants because of Rice.

2. Exception frequency - I can write a function that has "raise new FooException()" in the code, but the function never raises, and you won't be able to prove it never raises.

[wisty]

Well, you won't always be able to prove that it never raises. In many cases, you can, which is why compilers can eliminate dead code. Sometimes the compiler can prove the code is dead, sometimes it can prove the code is live, and sometimes it just doesn't know. For any prover, there will be code that defeats it.