> No, that's just not true. If you have an order relation (a Boolean lattice, in fact), and B => C, then if A => B, then A => C. I.e., any proposition C that is true for your level-of-detail B, then it is also true for your finer level-of-detail A.

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. We might have analysed programs X and Y in terms of their input and output and concluded they both print the same output when given the same input. But X uses mergesort and Y uses bubblesort. 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. The only way a formalism could let us reuse our analysis is if that formalism made us do all the work we'd do to compare the runtime even when we only want to compare the output. There's an excluded middle here.

> For one, the lambda calculus alone does not really describe a computation. Only a lambda expression combined with a state-machine -- i.e., an evaluation strategy -- defines a computation.

You do indeed need a description of how the computation is performed - an operational semantics - 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. The whole point of the Church-Turing thesis is that state machines and expression reduction are equivalent descriptions of computation.

> this style allows you to write your program however you like, and only then prove things about it, rather than write it with specific properties in mind (e.g., if you want to prove worst-case complexity, you must either write your program as a monad or use types that include a cost model).

This attitude has never made sense to me. 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. If I've got a requirement for a particular worst-case complexity, I can't write any useful subcomponents without thinking about worst-case complexity; I want worst-case complexity to be visible for every line I write, as soon as I write it.

> A "term-reduction system", more commonly called an abstract rewriting system, is also a state machine.

No it isn't. It's a different formalism for describing computation, per Church-Turing. 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.

> You get that anyway. Even in Java. That was precisely what Christopher Strachey showed when he first introduced the term "referential transparency" to programming languages[1] -- that imperative languages are referentially transparent. In Java, if you have an expression e, you can replace any sub expression, x, with another y, that has the same denotation, without changing the denotation of e. The difference between Java, Haskell and TLA is just what that denotation is. In Haskell, it is a "partial function"; in Java it's a predicate transformer [3] (i.e., a Hoare triplet); in TLA it's a set of sequences. This choice has both aesthetic and prgamatic consequences. I completely agree that the functional denotation and the behavior denotation are both normally more convenient than a Hoare triplet.

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. To be able to meaningfully talk about denotational semantics for a language, the semantics of a sequence of symbols in our denotation should match the way the sequence of symbols is understood by a reader, otherwise we just have two different languages that use the same symbols - and I don't think most people would read a line of Java and understand it to mean a Hoare triple. I'm not even convinced you've produced something compositional (GCL programs are just sequences of statements and can be composed by concatenation, so the Hoare triple semantics is valid for them, but Java programs are not structured that way), so it may not be a denotational semantics at all.

> you always "work on terms" when working syntactically

Exactly - what I'm saying is I want a toolset that makes it easy to work syntactically. 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. I want a denotational semantics where things that look like function application denote function application, things that look like equality denote equality, and so on.

> It is 100% false that a semantic domain of partial functions makes your state space in any way smaller than if your semantics domain is sets of behaviors.

There are only 9 possible partial functions of type Boolean => Boolean, whereas there's a combinatorially huge number of possible behaviours. But most of the time I don't even have to reason about the specifics of a function, because just knowing that it is a function - that applying it to the same input always means its return value when applied to that input - provides me with enough information to greatly simplify the space of possibilities to think about. If I have some code like:

{
val a = f(2, 4, 5)
g(a, a)
}

versus

g(f(2, 4, 5), f(2, 4, 5))

then if my syntactic function application denotes function application I can immediately conclude these expressions are equivalent, and I've only had to think about a few lines. If the thing that looks like function application actually denote state transformation behaviours then I have to reason about the space of possible states, which will always be huge.

> Haskell's type system (without clever tricks such as singleton types) is so weak that the properties it "verifies" fall far, far below what is normally regarded as "formal verification".

Be that as it may, what I said stands: properties of program fragments are formally proven, in a verified way, in normal industrial code, every day using Haskell-like type systems. No other approach can say that; Eve may be aiming for mainstream but it's nowhere near as mainstream as Haskell. 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.

> This is just mathematically wrong, because if you think of the cardinality of functions you'd realize that it's the same as (normally bigger, actually) than that of sequences (e.g. the set of functions from the natural numbers to the natural numbers is exactly that of sequences of natural numbers).

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. Whereas to understand the composition of two functions I only have to understand the return value of the first function, and that's generally taken from a much smaller space of possibilities than the space of possible program states. (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).

> Here are Xavier Leroy and Simon-Peyton Jones bemoan that the state of formal methods in FP is so far behind that of even "classical" imperative programming languages [4].

I don't do videos; I'll happily read written stuff but that talk didn't seem to be listed in the slides section of that site.