4 ms·

Why would an OS need to be Turing complete?

• eru 2y ago
  Yes, that wouldn't necessarily be a problem. Of course, getting a computer that's useful in practice out of this would require some thought. A simple model: you could only allow programs written in Coq (or similar), ie progams that come with a proof of termination (or a slight generalisation, that allows for infinite event loops, as long as each run threw the loop behaves well, in some sense). There's a trivial escape hatch, where you just take your normal unproven program but forcefully terminate it after 2^64 steps. That's strictly speaking not Turing complete, but you wouldn't be able to tell the difference during the lifetime of the computer.