> No, that's not true, because equality and equivalence aren't the same. You can work with an equivalence relation knowing full well there are finer equivalences (think, e.g. of quotient types). In fact, in a partial order (like a lattice), for every element a, we can define an equivalence relation ~a, s.t. x ~a y iff x ≤ a and y ≤ a, i.e., all elements less than a are ~a-equivalent. You can work with programs like that, saying, e.g., that a is "any program that sorts", and so all sorting programs are ~a equivalent. Still, theorems that make use of this equivalence relation (or any other) do not assume that it's an equality relation.

Well, sure. 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. The fact that I don't have to switch formalisms to talk about runtime doesn't actually help me, because I still have to redo all my analysis.

> A state machine is not a Turing machine. It is anything that has states (e.g. expressions) and transitions between them (e.g. reductions).

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

> That inference rules (reductions) form computation was known since Leibniz in the 17th century.

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.

> Turing explained why that is -- because all formalisms and inference rules are special cases of state machines.

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.

> It's not always that simple. Suppose I ask you to write a sorting program and you come up with mergesort. You then notice that aside from just sorting it has the property of being stable for incomparable elements. That's something that's nice to be able to prove without rewriting the program.

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. Accidentally implementing a future requirement seems like a very rare coincidence.

> If I write a Java method that isn't pure, I don't think of it as a function. In fact, I rarely think of computations functions.

I suspect that's pretty unusual. I mean, it's pretty normal to call them "functions".

> It's not contrived at all, and it's rather intuitive: every Java statement is a transformation of program state.

The trouble is that "a transformation of program state" is not an easy thing to think about. It could do absolutely anything.

> How many possible partial functions are there for (Int -> Int) -> (Int -> Int)?

A lot, so a well-structured program wouldn't use a function with a signature like that. The space of possibilities for e.g. (a -> b) -> (a -> b) is much smaller.

> That's really, really good! But 1/ that still doesn't mean that purity needs to be enforced everywhere, and 2/ this helps but only with the easy part.

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.

> In that case, many, many more systems (many, many times over) are formally proven using Java-like type systems.

Sure, not that I'd really distinguish between the two at the level we've been talking at. That the Java type system has been successfully used extensively in practice is a good, hopeful thing about it - though that people commonly cite Java's verbosity as a reason for leaving the language is a mark against that. Unfortunately I've found that in practical Java programs one almost always needs to go around the type system and/or can't practically represent important properties like "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. 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. Not some radical new model to learn, just ordinary functions with ordinary return values the way every industrial programmer is already used to thinking about the easy parts of their program with and a few clever techniques to allow us to extend the same approach to work on the hard parts as well.

> You can try to imagine what that system would look like or you can read my posts/watch my talk. You're not actually dealing with the elements of sequences as you may imagine, just as you're not dealing with sets of pairs when you're analyzing functions. We're talking about an elegant algebra of program behaviors, that I don't wish to fully describe in a HN comment, partly because I've already described it elsewhere.

I've tried to read your posts, repeatedly. I just struggle to find the "there" there; I have no intuitions about any of these objects that don't boil down to the same thing as your shadow-variables-and-assertions example; I can't see what they're supposed to do for me that plain old functions and values and types make hard - I can't even do the things that were previously easy.

> the fact that you can easily reason about sequential programs is very nice, but most programs today aren't sequential, and so we get to tradeoffs again

I'm just not convinced there's a balanced tradeoff here. To do functional reasoning you keep a natural, familiar semantics (functions as functions and so on) in plain-old mathematics that you already use when reasoning about the easy parts of your program, you factor out commonality as functions the same way you already do when programming. We're talking about making a few small generalisations of the type system, that's all. 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.