> I'd be impressed if you gave me a program for which it provably cannot be proved that it halts. Or a bound on its size.

For every program that halts, it's obviously possible to prove that it halts. The point is that there is no algorithm for deciding if an arbitrary given program halts.

> there is no algorithm for deciding if an arbitrary given program halts.

But can you prove that statement if I change it into:

there is no algorithm for deciding if an arbitrary given program with size less than N halts; for some suitable definition of size.

Since we're considering practicality, let's change the statement to: “There is no algorithm for deciding if an arbitrary given program with size less than 1000 bytes halts which can be implemented without solving several famous open mathematical problems”. I think my program pretty clearly shows that this is true.