> The halting problem applies when you are trying to check the properties of arbitrary programs. However, we are not writing arbitrary programs, we are writing very specific (hopefully useful) programs. The two are very different.

No, they aren't -- they are all Turing-complete, look it up. The THP applies to all non-trivial programs, meaning programs that support Peano arithmetic or anything more involved. That limitation certainly applies to all the programs you're describing.

> Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole.

That's pretty funny. It's not every day I hear Alan Turing and Kurt Gödel described as purveyors of "pop-sci".

> Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."

I won't try to list all the logical fallacies in your argument. You could do that if you were so inclined.