On a related note, I have the impression many people don't really understand the implications of the halting problem. You often hear the famous sentence, "it's

On a related note, I have the impression many people don't really understand the implications of the halting problem. You often hear the famous sentence, "it's impossible to build a program which decides whether another program holds", and use this as an argument that any attempt at building such developer tooling is futile. But in fact, the whole proof is based on the self-application problem, where it's roughly analogous to the liars paradox. But the proof doesn't say anything about other, non-"reflective" cases. Theoretically, it might be possible to build a program that makes correct decisions whenever that's possible, and otherwise ends up in an infinite loop (e.g. in the self-application case). I wonder if there are any efforts in this direction; so far I've never heard of it.