> If that were true there would be no point talking about language design at all.

Why not? People talk about music, art and, well, design, all the time.

> the programming community does manage to eventually achieve rough consensus about which language designs are good and which are bad

That still doesn't mean there's no large aesthetic component.

> ultimately there is a fact of the matter when it comes to productivity, however difficult we find it to actually measure.

I agree, except that very large differences in just about anything are pretty easy to measure. I think it is almost an established fact at this point that no great differences in productivity exist between modern languages.

> Identifying expressions with their reductions (i.e. their evaluation) does not come cheap, but it pays a huge dividend in terms of how much it simplifies the space that we need to reason about

All formalisms have expressions and reductions. Their denotation is just different. For FP it's so-called "partial functions" (which resemble computable functions); for classical imperative languages it's Hoare triplets (or some other mathematical object). It's just that the denotation offered by lambda calculus is inconvenient when it comes to interactive/concurrent/distributed programs, precisely because the lambda calculus itself cannot directly represent any of them in its reductions, rather delegating them to externally defined mechanisms (IO types, message passing etc.).

> and my experience is that this does not just benefit the formal model, it helps the human programmer's reasoning in the same way.

I agree, but lambda calculus is quite bad at this compared to alternatives. Where it's good -- sequential programs -- not much help is needed. You can have immutability and the thing FP advocates mistakenly call "referential transparency" (when they really mean a simple denotation) in formalisms that are much better suited to modern programming than lambda calculus.

And I really wouldn't mind saying, well, LC doesn't help with the hard stuff, but it does help with the easy stuff, so we should all adopt if there had been any evidence that pure FP yields a large benefit, but there isn't.

> I've found that bug incidence has gone way down.

I believe you, but think that your experience isn't at all universal. Others may find employing better discipline (including precise and even formal analysis of programs/algorithms) in the languages they like to yield more of an impact, while adopting a very different programming style to be a distraction that just hurts overall productivity.

> I don't think I've ever seen this "looping monad"; certainly what you're describing doesn't sound at all like the usual state monad. Could you point towards an implementation of the kind of monad you're talking about?

Ugh, you made me look up Haskell syntax :)

So, you can have:

fac1 :: Int -> Int
fac1 0 = 1
fac1 n = n * fac1 (n-1)

fac2 :: Int -> Int
fac2 n = go n 1 1
where
go n i x = if i <= n then (go n (i+1) (i*x)) else x

fac3 :: Int -> Cont r Int
fac3 0 = return 1
fac3 n = do
a <- fac3 (n-1)
cont $ \k -> k (a * n)

fac4 :: (Int, Int, Int) -> State (Int,Int,Int) ()
fac4 (n, i, accum) = put (if i < n then (n, i+1, i * accum) else (n, i, accum))

(fac4 doesn't really express the full computation, but I wanted to make clear what's going on; fac3 is a better, though less clear example)

All really express the same computation -- the operational semantics are isomorphic (I could have gotten some of the details a bit wrong, but in general) -- but the functional denotation does not express that. Even in classical imperative languages the denotation (say, using Hoare triplets) is isomorphic. The reason is that the functional denotation, is, well, a function and not a computation. This is a great simplification in sequential programs, but becomes very problematic when interaction/concurrency is involved.

> That aside, the normal representation of recursion in the lambda calculus is already that you form a structure that represents the recursion to happen and then pass it to an operator that actually does the recursion (a Y combinator or similar)

1. FP programming languages are not really Church’s lambda calculus, and the Y combinator in them is implicit. You cannot define a Y combinator in a typed LC. (scratch that -- this is wrong; see comment below)

2. The problem exists even in “proper” LC, as passing the “step function” to a Y combinator or in a monad still yields isomorphic operational semantics that are incomparable types.