So why are you upset when I say that I don't find pure FP to be appealing or convenient for concurrent/interactive/distributed programs? I think that the very notion of representing computation as functions in such circumstances is ill-advised, and results in a very inconvenient, very unnatural (at least for me), and very hard-to-reason-about formalism compare to alternatives. Nevertheless, my opinion is subjective, and I can accept that some may not share it.

> If expanded on that as much as you have expanded on the semantics of Haskell in this thread then we might actually learn something very interesting!

I did. Read my blog post (which is the general theory), and then read the Dedalus paper. Some time ago you asked me to write something about TLA(+). I have, my posts (especially parts 3 and 4) are aimed precisely to get people away from what Lamport calls the "Whorfian syndrome", which is confusing the analysis of a particular formalism with that of computation or programs in general. In addition, I strongly recommend reading the overview paper, Binary Relations for Abstraction and Refinement [1] by David A Schmidt (who also wrote the book Denotational Semantics: A Methodology for Language Development). While the last section of that paper discusses temporal logic, the paper really applies to all programs in all programming languages.

[1]: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16....