>> the halting problem proves that you can never prove a program halts

Halting problem proves that you can never prove an "arbitrary" program halts. A specific program can of course be proven to halt or not halt.

The above statement is often misused to state that day-to-day PC programs can never be proven to be bug-free (even in theory).

Aye, I always think of the halting problem as "if the program is still running, you can't necessarily know if it will ever halt." If you see a program halt, after a millisecond or after 10 years, then you've obviously proven whether or not it halts.

Also, while the halting problem doesn't necessarily say anything about bugs, there is a more general theorem that essentially says that you can't know in general if a program enjoys any non-trivial property (e.g. it prints a "1" at some point, it accesses the network, or it halts). I can't recall the name of the theorem, but the intuitive proof is similar to the halting problem's. This theorem does seem to hint that programs can't be proven to be bug-free in general.

>...there is a more general theorem that essentially says that you can't know in general if a program enjoys any non-trivial property....

That would be Rice's theorem. http://en.wikipedia.org/wiki/Rice%27s_theorem

There are several classes of programs that can be proved to halt. Any non-recursive program without a loop halts. In addition to that, our research group in grad school showed that some looping programs can also be proved to halt as long as they are marked with loop termination clauses that can be proved to hold for the program in question. Look to Ohio State RSRG for more info.