> Fundamentally, many pairs of real programs are equivalent at a coarse level and inequivalent at a finer level, so no formalism could ever escape that.
You keep saying that, but TLA is a formalism specifically designed to do just that. It defines a lattice of algorithms, where one is "smaller" than another if it is a refinement of it.
> If we now want to compare the runtime of X and Y, we can't reuse our analysis, because fragments that we previously considered equivalent are no longer equivalent, symmetries that we previously made use of are now broken.
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.
I don't want to presume, but you maybe you're just used to a formalism where the only equivalence (on the denotation in that formalism) is equality (the extensional function equality). To make this more familiar, I can point out that typed functional languages also have weaker notions of equivalence, as they have one level of abstraction/refinement (assuming no subtypes) -- that between types and their inhabitants; the relation between type parameters and concrete types might be another level, as is typeclasses. You normally have theorems about functions based just on types, and that are true for all inhabitants (or theorems about a polymorphic signature that is true for all type instances). You don't need to rework your theorems for every type inhabitant (or every type instance). In a formalism like TLA, this abstraction/refinement relation is a lattice with infinite levels (a little similar to a formalism with subtypes). Instead of just having types (which express nondeterminism, i.e., the type Int -> Int nondeterministically represents some Int -> Int computation) and inhabitants, you have arbitrary levels of nondeterminism (or abstraction), where more refined programs can be instances of more abstract ones (i.e., ones with more nondeterminism).
> but state machines are not the only form of computation. For the lambda calculus reduction is evaluation - what you did in https://news.ycombinator.com/item?id=15786021 was computation, with no state machine in sight.
Evaluation is a state machine. The substitution I did -- that's a state machine. A state machine is not a Turing machine. It is anything that has states (e.g. expressions) and transitions between them (e.g. reductions).
> The whole point of the Church-Turing thesis is that state machines and expression reduction are equivalent descriptions of computation.
Not quite. That inference rules (reductions) form computation was known since Leibniz in the 17th century. Church's claim was that even the simple reductions of the simple lambda calculus can express any computation expressible by any formalism. Turing explained why that is -- because all formalisms and inference rules are special cases of state machines. Gödel then called Turing's explanation "a miracle", as for the first time we had a definition of what a formal system is and how it works.
> Of course I'm writing my program with specific properties in mind - I'm not just writing some random program and then seeing what properties it has, I'm writing the program because I need a program with certain properties.
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.
> You can simulate one with the other, but neither subsumes the other; a rewriting system isn't a state machine any more than a state machine is a rewriting system.
A rewriting system is very much a state machine (albeit often a nondeterministic one, due to evaluation order).
> Any collection of symbols can be given a trivial "denotational semantics", but this "denotational semantics of Java" would not capture the things that make Java Java, because the relations between "expressions" (which would not correspond to Java expressions) bear no relation to the definition of Java-as-it's-usually-understood, the denotations of Java functions would not be functions.
I don't know where you get that. Formal methods for Java (like Infer [1]) make use of this denotation all the time, and programmers who carefully think about their Java programs do it just as effectively as those who carefully think about their Haskell programs. Sometimes their work is harder, and sometimes it isn't, and in any event, there are many other considerations to take into account (e.g., analyzing programs from syntax is not the only nor the "best" way to analyze programs; we also analyze programs as they run using dynamic analysis tools, profilers and tracing).
Of course the denotation of Java methods isn't functions. The standard denotation for imperative languages is that of Hoare logic (or "Predicate transformer semantics" [2]). 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 want referential transparency in terms of the common-sense meaning of the syntax, not in terms of some contrived meaning that exists only for analysis.
It's not contrived at all, and it's rather intuitive: every Java statement is a transformation of program state.
Now, I completely agree with you that functional semantics are more convenient (as they're simpler, more local etc.), but they stop being convenient once the program isn't sequential. The question is, is it worth it to use a language that enforces (by enforced purity) this function semantics on the entire program if it's only really helpful for some bits of it. There is no right answer to this question. Some would prefer that language and some wouldn't, and both would be perfectly justified.
> There are only 9 possible partial functions of type Boolean => Boolean, whereas there's a combinatorially huge number of possible behaviours.
How many possible partial functions are there for (Int -> Int) -> (Int -> Int)?
> and I've only had to think about a few lines
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.
> properties of program fragments are formally proven, in a verified way, in normal industrial code, every day using Haskell-like type systems.
In that case, many, many more systems (many, many times over) are formally proven using Java-like type systems.
> I'm a lot more confident in our ability extend that approach to cover the properties we care about, than in our ability to get the overhead of state-oriented approaches low enough to use for normal industrial code.
That's an overhead that you're imagining. In fact, it's much easier to build formal tools for what you call "state-oriented" approaches than for pure functional languages because of the latter's dependence on higher-order functions.
> Just thinking about sequences of state operations doesn't tell me enough to understand a program; I can't understand the composition of two sequences of state operations without understanding the full state... Of course a state operation is equivalent to a function from program state to program state, and such functions would be just as hard to understand as state operations - but most functions are defined on much smaller spaces
Look, you're trying to extrapolate from bits of information. We're talking about a system that's based on temporal logic, by far the most useful logic for formal methods to date, and one that has so far directly yielded two Turing awards. 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.
Anyway, once again, I'm not by any means trying to claim that Java is better than Haskell or that Eve is better than Haskell etc. I'm just trying to say that your conlusions (that Haskell is better than Java) are based neither on a good theoretical justification -- 1/ 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, and 2/ you seem unfamiliar with the vast body of research on other kinds of program analysis; AFAIK, nobody claims that those other methods are any "better" or "worse" than the functional one; just different -- nor on any empirical data (which is far more important). I just don't like this discourse that X is better than Y without a careful definition of what "better" means and without some very compelling evidence.
[1]: http://fbinfer.com/docs/separation-logic-and-bi-abduction.ht...
[2]: https://en.wikipedia.org/wiki/Predicate_transformer_semantic...