> But showing that two programs are ~-equivalent will be no help in attempting to show that they do (or don't) have the same runtime.

I'm not sure what you mean by "runtime" -- perhaps something equivalent to Haskell operational semantics -- but in other formalisms the entire system is different. For example, in TLA there is no distinction between the "runtime" and the "function denotation" -- these concepts simply do not exist -- they are both arbitrary points in the same denotational lattice. You can even say that A and B are two different refinements (implementations) of Quicksort, B and C are refinements of Mergesort, and all four are refinements of Sort. What is true for Sort is true for all four. What is true for Quicksort is true for A and B. Those are just arbitrary levels of abstraction. There is no defined concept of "function" which is a specific level of abstraction.

> "State machine" is generally understood to mean a finite state machine i.e. a Turing machine.

A Turing machine is certainly not a finite state machine, and abstract rewriting systems are also state machines. In fact, if you'll google for papers on the operational semantics of lambda calculus (or related PLs), I'm sure the term state machine will come up.

> Indeed; they are if anything the most natural definition of computation, contra your description of computation as a physical process. The "miracle" of Church-Turing is that the mechanistic finite state machine is equivalent to the more natural rewriting system, paving the way for mechanical computation.

Where "more natural" meaning you like it better because that aesthetic appeals to you :) There is just no accepted standard here. In fact, vast subfields of CS never consider the formal-system description, and they are much, much larger than those subfields who prefer working in formal systems.

> He didn't show anything about a state machine in your generic sense of "anything that has states and transitions between them". He showed an equivalence between reduction and finite state machines. Neither is a special case of the other, they're just equivalent.

Not quite. Read his paper, it is very readable. He defines (for the first time!) a general notion of computation, and from it creates an arbitrary instance of it (which is not a finite state machine) which we now call "Turing machines" just for the sake of rigorous mathematical analysis. Turing was the first to define computation in general.

> If stability was part of the requirements I would've wanted to pay attention to it all along; if it wasn't then it's unlikely to become one.

My experience has been different.

> I mean, it's pretty normal to call them "functions".

First, they're not called functions in Java, but "methods", but let's say C. It's pretty normal to call Haskell functions "functions", even though they're not. The term "function" in programming has a long history, and it's because the idea resembles mathematical functions. I agree Haskell functions resemble mathematical functions much more than C functions, but neither of them are actual functions.

> My experience has been that it can all, or almost all, be put in the easy part. I just haven't had these problems with nonsequentiality that you claim. Maybe there's a niche where they're important, but I don't see the use case the broader industry - webapps, business process automation, that kind of thing.

Well, we've had different experiences, then, but I don't need to trust my experience. There's no evidence that writing applications in Haskell is significantly cheaper than writing them in Java or Kotlin.

> "this function is only called during an open database transaction" or "this object graph contains only objects that we know how to represent as JSON", due to lacking monads, lacking records, perhaps due to lacking purity.

This is actually easier in Java than in Haskell. That's what JML[1], arguably the most sophisticated contract system out there, is for (although, admittedly, very few people use it; then again, very few people use Haskell). I don't know why you keep bringing up monads when they are a feature of a formalism, not a general solution to a problem.

> To achieve the defect rates I believe the industry will need in the future, I believe we need a couple of small extensions over the Java type system: higher-kinded types, some form of record-like types (i.e. the ability to work generically with maps where the type of each value is known, but different for different keys), maybe linearity, maybe polykinds.

The difference is that I come from a formal methods direction. I don't look at solutions just in FP. I look at the entire formal methods field and see which solutions are promising for the problems. While I don't know if any would work, both research and a few decades of experience in safety-critical realtime systems show that the synchronous approach, now taken by Eve, is much more promising from a correctness perspective. If your only point of reference is FP, I don't know how you can claim that the (quite clunky, IMO) solutions FP comes up with are the best way forward. Read up on what the general formal methods community is reasearching so you'll have something to compare the FP approach to.

> It's such a small step, but it's enough to let you prove so many of the things you actually care about in plain old industrial programming; I really can't see why a Java or Kotlin programer would prefer to jump to analysing their programs with a whole new formalism; that seems like a much bigger cost, and there's no visible space for it to have a correspondingly greater benefit.

They don't need to jump anywhere. The current formal tools for Java are far more sophisticarted than those available for Haskell. That people don't use them is a different matter, but it's both a shorter jump and arguably a similar if not greater benfit to go from programming in Java to programming in Java and running a static analyzer than to go from programming in Java to programming in Haskell (even assuming Haskell was no worse than Java in any regard, and I find that this is not at all the case).

[1]: http://www.openjml.org/