> But there is much to be said against PFP itself (and much to be said in favor) like the lack of clear execution models, the lack of clear thread context (which is, of course, related), the difficulty in analyzing computational complexity, in debugging and profiling, and implementing many simple algorithms. Many of those are related to laziness more than referential transparency itself, but RT necessitates laziness in some cases, whether the language itself is strict or not.

Don't blame purely functional programming and referential transparency, which are unquestionably good ideas, for the downsides of laziness, which is indeed a bad default. Purely functional programming doesn't need laziness, and, in fact, is much better off with a formal distinction between values and computations, as in the call-by-push-value paradigm [0]. Pervasive laziness actually has negative consequences for equational reasoning, because it forces all free variables to stand for potentially nonterminating computations. To restore the practicality of equational reasoning, Haskellers often have to pretend free variables only stand for productive computations (that big-step-reduce to a term in WHNF), but this assumption is completely unwarranted by language itself.

> "wherefore referential transparency". If it is to avoid problems caused by shared mutable state, then there might be better ways, like making shared state transactional to some degree (Clojure, Erlang).

Although it doesn't exactly have transactions, Rust's strict aliasing and mutability controls is a much better argument for "there are better ways to avoid the problems of shared mutable state". Clojure and Erlang take the easy route of making the consequences of your bugs less catastrophic [1], but do very little to actually avoid concurrency bugs.

> If it is to make automatic verification better, then there might be easier ways (like some of the many model-checking methods)

Model-checking doesn't scale to truly large state spaces. Typeful purely functional programming is, to a large extent, about trimming the state space to exclude nonsensical stuff.

> and if it is to make human reasoning better, one should ask whether equational thinking is really the best way for people to think about programs

Yes, equational reasoning is the best way for people to think about programs. Equational reasoning, being barely more complex than high school algebra [2], is so easy that a normal programmer can do it casually. The most complicated operation you ever have to perform is substitution: replacing all free occurences of a variable by an expression.

> (I think the human mind is much more adept at simulating state than at math, and that an essential, "basic" abstraction such as monad transformers is already too high-order for people to wrap their heads around)

The untrained human mind might be more adept at simulating a single sequence of states than at math. However, even the best trained human mind is comically bad at analyzing classes of sequences of states, formally or informally. In particular, in the formal case, this kind of analysis often requires using logical relations, such as weakest preconditions [3], whose bodies can contain arbitrary quantifiers. Now, as anyone who's used formal methods can attest, rigorously manipulating quantifiers is a bitch - you often have to refer to their formal rules of inference, because it's so easy to use quantifiers wrong if you rely on intuition alone.

> I think that because much of PL research in the last decade has been focused on PFP, people are under the impression that it is somehow more "mathematical" or theoretically sound (not in the logical sense) than imperative, completely forgetting that fully-verifiable, and theory-supported imperative languages (like Esterel and its descendants) have been used much more successfully in the industry than Haskell and friends.

You're right that it's perfectly feasible to ground imperative programming in a formal foundation. However, as I explained in my previous points, in practice, the formal techniques for reasoning about functional programs are straightforward enough to learn and use by anyone straight out of high school, whereas the techniques for formally reasoning about imperative programs are both cumbersome and subtle - that's precisely why they aren't used except when incorrect programs are completely unacceptable.

> The argument of PFP vs. imperative is important and interesting, and there are both mathematical as well as psychological arguments to be made in favor of each. However, in recent years, many have come to see imperative as pedestrian and PFP as mathematically-advanced, which is completely false.

Again, I partially agree. Imperative programming is far from pedestrian. It's too complicated, in fact, so complicated that the only way we can cope with it is by handwaving away our proof obligation.

---

[0] http://www.cs.bham.ac.uk/~pbl/cbpv.html

[1] Erlang's marketing is very honest about this: Let it crash.

[2] The extra complexity comes primarily from the fact that high school algebra is single-sorted (all free variables are real, or at most complex), whereas equational reasoning in Haskell is multi-sorted (because Haskell has a rich type system).

[3] https://en.wikipedia.org/wiki/Predicate_transformer_semantic...