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.
That means we can't make the claim that a particular program, running in that language, is error-free. I don't get why people find this so hard to understand.
> That would imply you could never know anything about a program.
No, it means we can't make the claim that a program is error-free. That's the simplest statement of the Halting Problem.
When someone applies Lean to verify the correctness of a chain of logic, they must remember than Lean cannot be proven to be error-free, because ... wait for it .. Lean is Turing-complete.