I don&#x27;t think at all that &quot;value semantics&quot; without any mention of complexity is an end in and of itself. Any sensible programmer will either (a) intentionally decide that performance is minimally important at the moment (and hopefully later benchmark) or (b) concern themselves <i>also</i> with a semantic model which admits a cost model.<p>Or, to unpack that last statement, simulate the machine instructions.<p>I&#x27;m never one to argue that a single semantic model should rule them all. Things are wonderful then multiple semantic models can be used in tandem.<p>But while I&#x27;d like to argue for the value of cost models, at this point I&#x27;d like to also fight for the value-based ones.<p>Totality is important not because it has a practical effect. I vehemently agree with how you are arguing here to that end.<p>It&#x27;s instead important because in formal systems which ignore it you <i>completely</i> lose the notion of time. Inclusion of non-termination and handling for it admits that there is <i>at least one way</i> which we are absolutely unjustified in ignoring the passage of time: if we accidentally write something that literally will never finish.<p>It is absolutely a shallow way of viewing things. You&#x27;re absolutely right to say that practical termination is more important that black-and-white non-termination.<p>But that&#x27;s why it&#x27;s brought up. It&#x27;s a criticism of certain value-based models: <i>you guys can&#x27;t even talk about termination!</i><p>And then it&#x27;s also brought up because the naive way of adding it to a theorem prover makes your logic degenerate.