There’s a fairly interesting way of solving these issues that might be worth thinking about: treat non-termination as a side-effect.
This means that instead of having semantic interpretations like {{bottom, “”}}, you have ones like {{_, non-termination}} where a side effect occurs and no value is available. What’s nice is that now the value-level semantics are simple—they don’t have any weird explosions like bottom (ignoring, for the moment, 1/0, which is more malformed than exceptional).
Non-termination as a side effect is strange because you can’t observe it. There are two ways to approach an escape from here. First, you can examine what the normal practical way of “observing” non-termination is: you give up on it after a time and call it non-termination. This is “termination by impatience” or merely accepting the finite resolution power you have.
The second is to reify impure things as pure values as is done in effect-handling languages. Now, termination has a pure semantics… the standard one is to require any observation of the impure, potentially non-terminating code to be specified alongside some amount of “fuel” which describes how long you’re willing to wait and, potentially, offers a suspended computation when the fuel runs out so that you can continue it.
There’s a fairly interesting way of solving these issues that might be worth thinking about: treat non-termination as a side-effect.
This means that instead of having semantic interpretations like {{bottom, “”}}, you have ones like {{_, non-termination}} where a side effect occurs and no value is available. What’s nice is that now the value-level semantics are simple—they don’t have any weird explosions like bottom (ignoring, for the moment, 1/0, which is more malformed than exceptional).
Non-termination as a side effect is strange because you can’t observe it. There are two ways to approach an escape from here. First, you can examine what the normal practical way of “observing” non-termination is: you give up on it after a time and call it non-termination. This is “termination by impatience” or merely accepting the finite resolution power you have.
The second is to reify impure things as pure values as is done in effect-handling languages. Now, termination has a pure semantics… the standard one is to require any observation of the impure, potentially non-terminating code to be specified alongside some amount of “fuel” which describes how long you’re willing to wait and, potentially, offers a suspended computation when the fuel runs out so that you can continue it.
Would it be easier to phrase it as termination is a side effect? Then require that programs not produce effects when they aren’t supposed to?
Of course, if c++ defines non termination as undefined, all bets are off.
(Potential) non-termination is the effect. If you’ve got known-terminating code then it can prove that property and be free of effect.