> The things that you want or don't want in order to maximize some value function are exactly what aesthetics is. There is no mathematical theorem, or no natural law, determining which value function I aim to optimize, and therefore no objective rule for deciding which language features are "correct", and no absolute measure for what constitutes good design. The only measure for good design is whether or not the product optimizes the value function that you've chosen on aesthetic grounds.

If that were true there would be no point talking about language design at all. I don't believe that; the programming community does manage to eventually achieve rough consensus about which language designs are good and which are bad, and ultimately there is a fact of the matter when it comes to productivity, however difficult we find it to actually measure.

> Think of writing a factorial function recursively and one using some looping monad. The two have isomorphic operational semantics, but completely different denotations. Monads basically let you express any kind of computation, including those that you can express with plain lambda terms. In addition -- and this is important -- some computations can _only_ be expressed with monads (assuming you don't have linear types). This means that lambda calculus contains two different, and incompatible, ways of expressing computation.

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?

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), so I don't see this notion that any monad-like representation would be substantially different.

> Formalisms invented for general (i.e., not necessarily sequential) computation, including sequential, concurrent and interactive, don't have this problem, and have just a single, simple and uniform way to express any kind of computation. This makes them amenable to mathematical analysis, something the pure-FP model has difficulty with (you'll note that when analyzing pure FP, various ad-hoc frameworks need to be invented, e.g., a message-passing model for concurrency etc.)

Your own talks have covered the theme that doing formal reasoning about the full operational state space of any nontrivial program is impractical because that state space is so large. If we're to hope to be able to do practical analysis of programs we have to have a representation that collapses that space hugely. 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 - and my experience is that this does not just benefit the formal model, it helps the human programmer's reasoning in the same way. Even back when I worked in Java, those things that don't fit neatly into the FP framework - concurrency, exceptions - were the biggest sources of bugs. And now that I've used FP-compatible abstractions for these things - however ad-hoc those abstractions were at first - I've found that bug incidence has gone way down.