alt Hacker News> 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.
The language is Turing-complete, not the program. Rice's theorem says that we can't have a program that verifies a non-trivial property for all other programs. It doesn't say we can't verify that property for some programs. That would imply you could never know anything about a program.