Wikipedia: [1] Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to produce contradictory output and therefore cannot be correct.
This is so reductive a framing as to be essentially useless [0]. I think maybe you want to learn more about program correctness, formal verification, and programming language semantics before you make such statements in the future.
[0] See, e.g., type-checking.
When is an OS supposed to halt? When you shut it down, or when you power down the hardware, and no other times. So if you don't do either of those things, then the OS is supposed to run forever. Does that, by itself, mean that the program is incorrect, or that the language is inadequate? No, it means that the definition is worthless (or at least worthless for programs like OSes).
This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.
Same way you can count to any finite integer with enough time, but you can never count to infinity.
Those kinds of interactive programs take in a stream of input events, which can be arbitrarily long, but eventually ends when the computer is shut down.
Termination checkers don't stop you from writing these interactive loops, they only stop non-interactive loops
Not possible for all problems. We cannot decide correctness (ie adherence to a specification) for all programs, but we can definitely recognize a good chunk of cases (both positive and negative) that are useful.
The Halting Problem itself is recognizable. The surprising result of Turing’s work was that we can’t decide it.
Keyword emphasis mine.