Hacker News new | ask | show | jobs
by AnimalMuppet 59 days ago
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).
3 comments
gopiandcode 59 days ago
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.
link
DonaldPShimoda 59 days ago
> finite programs that run on an infinite stream of events

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.

link
hmry 59 days ago
Two different meanings of "forever" there. An OS runs for an arbitrarily large finite time, which is different from an infinite time.

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

link
Rusky 59 days ago
This is not actually a problem for total languages, which simply model these kinds of processes using corecursion/coinduction/codata.
link