> Church's definition of the lambda calculus actually slightly predates Turing's definition, and Goedel's definition was even earlier. There are bidirectional equivalences between all three; neither is an instance of the other.

Read the papers, then. You'll find striking differences between Church's and Turing's papers. For one, Church doesn't define what computation is. Instead, he attempts to justify why the lambda calculus is universal, and even then he gets caught in circular reasoning, at which point he gives up and writes in a footnote something like, well, if I can't do this, I don't know how anyone can define computation. Turing's paper, however, was one of the biggest philosophical breakthroughs at least since the 17th century, and regarded by Gödel as a miracle. It is true that Church published his proof of the undecidability of logic ahead of Turing, but his paper does not contain an analysis of what computation is, whereas precisely that is considered the main achievement of Turing's paper.

> I would think Haskell is substantially more popular than JML, though I could be wrong.

I would think so, too, but it's still very fringe.

> I did make an effort to use a contract-based system with Java code and found it was ultimately harder than switching languages. Partly that's a question of tooling, but I think the biggest barrier was the semantic model.

I've had the opposoite experience. Even if Haskell dominated Java as a language (which I absolutely don't think it does), I wouldn't consider it worth switching because the bottom-line benefits are too small (if they exist at all), while the tooling and ecosystem (both libraries and hiring) is so lacking that the significant hit would dwarf any gains.

> The things FP does are largely just the application of widely agreed programming principles - separating concerns, making each function do one thing, explicitly distinguishing interface from implementation.

I disagree that FP has any advantage here over most programming languages.

> I can't imagine wanting to not have monads or records, and the minor type system enhancements needed to accommodate them seem like such a tiny cost compared to the benefits.

First, most languages have records (including Eve and TLA+). Second, monads are completely meaningless and useless once functions are not how you describe computation. They are very much a formalism-dependent construct. Lastly, while I like type systems, I think about the problem not the solution. The problem is cheap specification and verification of simple propeties. Types are not the only way of doing that, and when considering the future of programming, we cannot constrain ourselves to solutions found within a very narrow sub-discipline while ignoring the full body of research.

> I feel like I gave a fair test in terms of the time and effort I put in - if anything I put much more effort into trying to use the non-FP approaches. FP solves the problems I have, and I didn't have to stop working and learn a new formalism; I was able to incrementally get there, starting by doing the same stuff I was already doing in Java, and remaining productive every step of the way. Whereas I sunk hours into thinking about preconditions and postconditions and never got anything out of it.

I fully believe that. I've had the exact opposite experience, ever since starting to work with Scheme and SML almost twenty years ago. I don't think Java dominates Haskell and I don't think Haskell dominates Java. Each works better for different people and different circumstances, and there is currently no evidence that either is significantly ahead of the other in terms of the bottom-line.

I have no problem arguing for days over this feature and that, this design philosophy or the other. I just don't like claims that the evidence does not support.