&gt; A much more foundational difference of opinion about purity arises from whether or not you allow termination.<p>Termination or non-termination? One of the (many) things that annoy me about PFP is the special treatment of non-termination, which is nothing more than unbounded complexity. In particular, I once read a paper by D.A. Turner about Total Functional Programming that neglected to mention that every program ever created in the universe could be turned into a total function by adding 2^64 (or a high enough counter) to every recursive loop without changing an iota of its semantics, therefore termination cannot offer a shred of added valuable information about program behavior. Defining non-termination as an effect -- as in F* or Koka (is that a Microsoft thing?) -- but an hour&#x27;s-computation as pure is just baffling to me.<p>&gt; I&#x27;d be interested to see a semantics where setting mutable stores is sufficiently ignored by the choice of equality as to be considered a non-effect. I&#x27;m not sure what it would look like, though.<p>I think both transactions and monotonic data (CRDTs), where mutations are idempotent, are a step in that direction.