> 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 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_semantics https://en.wikipedia.org/wiki/Predicate_transformer_semantic...
> Don't blame purely functional programming and referential transparency, which are unquestionably good ideas
I think many people question that they are good ideas. Not pure functions -- but forcing all functions to be pure. If you do that, you are basically forced to use monads for all effects, and that is very questionable.
> 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.
Yeah, Rust does something nice, too, but every operation allowed by Clojure is also allowed by Rust. I don't see how it's any better. Erlang's "let it crash" has nothing to do with data-race bugs. Once you have a GC everything is a lot easier when it comes to concurrency. Rust works very hard to ensure safety without a GC, which is necessary for domains that can't use GCs (like programs in constrained environments). And in any case, I think most people would consider Rust to be even less functional or more imperative (whatever that means) than Clojure.
> Yes, equational reasoning is the best way for people to think about programs.
It's good that you're so certain about this, but I can just as easily say "running your program in a debugger and a profiler is the best way for people to think about programs". How do you know? And nobody has even shown that apriori reasoning is any better than posthoc reasoning (debugger, profiler etc.) Deciding that we must reason completely about our program before we ever run them completely ignores a whole set of useful tools that we have at our disposal.
I also challenge you to program the world's most used sorting algorithm, TimSort, with equational reasoning. And consider this -- Haskell is grossly insufficient to really reason about programs in this way. Idris is the very minimum to even start, and even that doesn't even begin to scratch temporal logic.
> replacing all free occurrences of a variable by an expression.
That is a mathematical argument. Not a psychological one. You could use the same argument to claim that teaching a person to catch a ball is easier if you teach them Newton's equations than let them practice. I mean, we know simply "replacing all free occurrences of a variable" is Turing complete, right[1]? Who says people are good at that?
> However, even the best trained human mind is comically bad at analyzing classes of sequences of states, formally or informally.
And yet 100% of production software in the world, including avionics, medical devices and the like is written in imperative languages. I am not saying this makes your claim outright wrong, but it certainly challenges it, especially considering little evidence exists PFP actually makes things globally better (i.e. not by fixing one undesirable property and introducing another).
> that's precisely why they aren't used except when incorrect programs are completely unacceptable.
But if you want to be honest, you must admit that PFP isn't used anywhere. Imperative verification is much more pervasive. And nobody said people writing programs are willing to invest any extra effort to make them more correct than they believe those programs need be. Programs need to be as correct as they are now only developed at a lower cost (although, if you could offer more correctness completely free -- without any negative consequence -- I don't think people would object).
> It's too complicated, in fact, so complicated that the only way we can cope with it is by handwaving away our proof obligation.
Again, you're thinking about it from a mathematical viewpoint, but mathematics has absolutely zero relevance to whether a programming language is a "good" one or not. It can only promise certain properties, not their desirability. Yes, imperative programming is too complicated for machines to verify in every circumstance, yet claiming it is too complicated for humans pretty much ignores reality (or, at the very least, requires some serious explaining). And where proofs are required, imperative PLs can be just as rigorously proven -- e.g. Esterel, which has been used successfully by the industry much more than Haskell. In other case, I don't see that we have any obligation for proof, and when we do, Imperative languages can do just fine.
What is the source of that obligation? Are, say, provably correct programs more important than fast programs? Than programs shipped soon but are only correct "enough"? Who says correctness is the most important concern? I can tell you that software users certainly don't think so. We had a correctness crisis in the nineties, but the transition to memory-safe languages and wide adoption of engineering practices have pretty much resolved it. It's gotten good enough that continuous deployment, or "how do we ship our software in ever shorter cycles" is now a much bigger concern for most companies than "how do we ensure our software doesn't have bugs". This isn't handwaving but what people actually want. I don't think math can tell them to want something else. It's great that you can build a perfect table, but it doesn't help me if what I need is a chair.
There is one domain, though, where correctness is important even in 99% of software which doesn't require absolute correctness: security. But even with security, memory safety has done a lot to make things better, and where it hasn't, dependent types would be necessary to prove correctness, anyway. You can also help with richer type systems in imperative languages, like Java 8's pluggable type systems[2].
To summarize, I think we know precious little about the relative merits of PFP vs imperative (and by imperative I also mean functional-imperative). Unfortunately, no one has ever used PFP to write any large software other than compilers, so we don't even have the beginning of empirical evidence to even start an educated argument on the subject.
[1]: Well, sort of -- the equivalence between LC and UTM is something many misunderstand. There are plenty of computations that can be expressed by a UTM and not in LC. LC is equivalent because it is powerful enough to simulate a TM (but most certainly not to directly represent any TM program), but from that point on your computational model is no longer simply substituting free variables.
[2]: E.g.: http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#tainting-checker http://types.cs.washington.edu/checker-framework/current/che...