> By that definition then you could call any operational semantics "denotational" and the distinction between the two would be pointless.

While there is some debate over what exactly can be called "denotational semantics", it is widely accepted that denotational semantics must display certain characteristics. Hoare logic does display those characteristics and is, AFAIK, considered denotational.

> in a well-factored functional-style program you can move the vast majority of program code/logic into those "least tricky parts", and have a machine-enforced separation between the two. So you can restrict the more expensive forms of analysis to a small subset of your code, and get a much better cost/benefit.

1. I know, but I don't find that approach appealing in the least.

2. Other approaches have the language and its theory cleanly deal with effects -- just as with computation -- and so don't require such a separation and actually help with the tricky effectful/concurrent bits because they were designed for that purpose. FP was designed for a different purpose.

> If you deliberately choose to use operations that are deliberately defined to not have a formal denotation then your code won't have a formal denotation.

But that is a feature of the functional formalism, not of all formalisms. All of these programs have the same hoare-logic denotation (in classical imperative languages), and the same behavioral denotation (say in TLA). A denotation is not a feature of an algorithm; it's a feature of the particular formalism used to express the algorithm (although some formalisms may possibly have more than one reasonable denotational semantics).

> IO is explicitly an "escape hatch" to be used as a last resort.

Yes, in the functional formalism. Not in every language. I wanted to show a particular property of functional languages that I find unappealing.

> E.g. if your model of IO follows our common-sense informal semantics (where we e.g. pretend concurrent access to the same file wouldn't happen - this is a choice you have to make when modelling, because in some contexts the ability of another process to interfere with fac.txt would be an important difference between fac1 and fac5 and we wouldn't actually want them to be equivalent)

Ah, but that's why I've specifically chosen this example. Other formalisms have no difficulty assigning simple and natural semantics in either case (and if we disallow concurrent writes but allow concurrent reads, all versions of the algorithm would have isomorphic denotations). The reason you run into any sort of difficulty here is because your chosen denotation is that of a function, and functions are not a good representation of interactive or concurrent processes. Other denotations used in other formalisms have no problem with that.

> So terminology aside, what's the problem?

There's no problem. I just want to point out why pure FP is not so well-designed for all circumstances, as, for example, its denotation is a bad fit in many circumstances. If you personally do find the aesthetics of FP appealing, and have no problem separating effects from computation, enjoying the benefits of pure FP for the pure computational part -- good for you! I was just trying to show why it is not a universally "better" formalism, and why there may be very good pragmatic and aesthetic reasons not to choose it.