[eru]

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.