> I would love to see PFP as a drawback and obtain its benefits without requiring its rigors.
> (One of) the real-world benefit(s) is that I can write a substantial part of a program and know from inspecting only a single line (its type signature) what effects it performs. How can OCaml give me that benefit?
That's a property, not a real-world benefit. It's like saying that one of the real-world benefits of Haskell is that its logo is green. In any case, don't know about OCaml, but in Java I just click a button, and get the call tree for the method (or, inversely, get the reverse tree for all methods eventually calling printf). More to the point, see some of Oleg Kiselyov's work on type systems for continuations here: http://okmij.org/ftp/continuations/
> I think that says more about how you interpret informal comments on the internet than it does about those making the comments.
I think that you should decide whether this is a serious discussion or grandstanding.
> Where did I say you should go (the equivalent of) "full vegan"?
Maybe you didn't say that I should, but you did say that it's better to be vegan (i.e. make a very significant "lifestyle" change without any evidence to its effectiveness).
> At least, it is not known to be wrong.
That's true. But I wouldn't go around telling people that being vegan has great health benefit if all we know is that it's not been found to kill you.
> I would love to see PFP as a drawback and obtain its benefits without requiring its rigors. So far I have failed to understand your ideas about how to do that and I can only continue to see PFP as a massive boon.
OK, but first, a few things: 1/ I don't know if by "rigors" you meant difficulties or rigorousness, but if the latter, then I don't see why you conflate rigor with the pure-functional abstraction. Most formally verified, safety-critical software is written in languages that are far more rigorous than Haskell, yet are not pure-functional. Which leads us to 2/ these are not "my ideas"; if correctness is your goal (as it seems to be), most languages guaranteeing correctness do not espouse the PFP abstractions. Haskell, Coq, Idris and Agda are used far less than other approaches to ensuring software correctness. Finally, 3/ I'd like to be careful when I say "benefits", because we don't know whether they are true benefits, neutral or even detrimental to software at large. All I can say that in this context, when I say "benefits" I mean things that I (and you) believe to be positive and see as potentially advantageous in the "real world".
Now, I will give you two examples (of languages used more than Haskell/Coq etc.) for "correct" languages, both of them are very rigorous in the sense of being completely formal, yet they do not suffer from PFP's downsides mainly by being measurably much easier to learn/teach/adopt. They are not generally applicable, but neither is Haskell. The first is the set of synchronous langauges, now used by the industry to design safety-critical realtime software, as well as a lot of hardware. Instead of PFP, it relies on what's known as the "synchronous hypothesis". It has been proven over three decades, as an effective, practical method of writing verifiably correct software by "plain" engineers in hundreds of critical real-world systems. You can read more about it here[1]. A generalization of the approach is called Globally Asynchronous, Locally Synchronous, or GALS, and I believe it has the potential of being a great, more widely applicable way of writing software in a way that lends itself to careful reasoning.
The second (you probably saw it coming), is TLA+. It's not a programming language, so I won't compare it to Haskell but to Coq. Unlike Coq, TLA+ does not rely on PFP, or Curry-Howard (neither do other verification tools, like Isabelle) but goes a step further in not being typed at all. It is not functional yet fully mathematical ("referentially transparent"), and its main advantage is that while having the same "proving strength" as Coq when it comes to verifying algorithms[2] while taking days to learn instead of months, and not requiring any mathematical background more than what any engineer already has. I guess that the answer to "how?" would be "in a manner bearing a lot of resemblance to the synchronous hypothesis".
There are, of course, other formal approaches (like CSP), but synchronous programming in particular has had a lot of success in the industry.
If you want to know about (typed) monads vs. continuations, and their relationship to typed effects, I'll refer you again to my blog post on the subject: http://blog.paralleluniverse.co/2015/08/07/scoped-continuati... and to Oleg Kiselyov's work, which I've linked to above.
[1]: http://link.springer.com/chapter/10.1007%2F978-3-319-11737-9...
[2]: Coq may be more powerful when proving general mathematical theorems, but Coq was designed as a general theorem prover, while TLA+ is a language for verifying software in particular.