And Alonzo Church proved in 1940 that you can avoid this problem by using a typed language in which all programs halt. But sadly some programmers still resist this.

▲

AnimalMuppet 3 hours ago | parent [-]

Some correct programs are supposed to run forever.

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).

	▲	gopiandcode 3 hours ago \| parent \| next [-]
		you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 (https://sel4.systems/) and certikos (https://flint.cs.yale.edu/certikos/), you simply model them as finite programs that run on an infinite stream of events.
	▲	Rusky 3 hours ago \| parent \| prev [-]
		This is not actually a problem for total languages, which simply model these kinds of processes using corecursion/coinduction/codata.