No, it is false. If all your functions were on simple types, then you would be correct (although the cardinality is still the same), but in order to express some programs using function semantics, you need to have higher-order functions, which vastly increase your state space.

> Proving things about denotational semantics is obviously easier than proving things about operational semantics. It's just less useful.

Again, what operational and denotational semantics are depends entirely on the formalism. The operational semantics of TLA don't even express the computation at all.

> There are finitely many partial functions between finite sets A and B but infinitely many sequences of state transitions that take states in A to states in B.

But the sequences exist in a lattice! I'm being very imprecise (to say the least; this is actually wrong, but conveys the idea) here, but just to give you an intuition, the sequence <1, 5, 6, 7, 8, 12, 0, 2, 1, 8, 6> is "smaller" in the lattice than the sequence <1, 6>. If your proposition is true for the latter, it is automatically true for the former. You never work with all possible sequences. In fact, there are infinite levels of them. Between any two states in a TLA+ behavior, there is an unbounded (yet finite) number of other states that are implicitly ignored. So what? The "state space" of which you reason is exactly the same as that of a "function" (assuming the function has enough information to prove the proposition, i.e., that it's not about complexity etc.).

> Be careful to pay attention to what lmm actually claimed. The claim was about "proof of properties of program fragments ... in "normal" industrial code ... ordinary webapps".

AFAIK, the only industrial grade, web programs etc., for which formal methods are used are Amazons AWS and some of Oracle's web services, that use TLA+. Whether or not someone uses Haskell, Haskell simply falls too short of "formal methods".

> Any language is referentially transparent if every expression is only denotationally equal to itself.

No, that's just not true. The only way that would work is if your denotation is the syntax itself, and that's just not what people mean when they talk about semantics in general. Template Haskell and Lisp are not referentially transparent. Regardless of what the denotation of term a is, you cannot replace it with any term b having the same denotation (and one exists unless your "denotation" is the syntax) while preserving the denotation of the complete expression.

> claiming the Java is referentially transparent is almost vacuous.

Except that the person who claimed it was Christopher Strachey in a seminal paper of programming language theory. No, it is not vacuous in the least.

> From there we conclude that Haskell's is more useful.

I know you very strongly believe that (and I do not), but there's neither the theoretical justification nor the empirical evidence (at least so far) to support that. From the fact that you can assign simple and clear semantics to some kinds of computation you most certainly cannot conclude that the formalism is more useful in general. It all comes down to aesthetics and pragmatics. You like Haskell better than Java (and I like Java better than Haskell), and you are more productive in Haskell than Java (and I'm more productive in Java). That's all. Unless we have evidence of either being universally more productive than the other, we simply cannot make such claims. And that's OK! You can evangelize Haskell showing people what you like about it and why you think it's great. I just don't like these sweeping claims that have no justification. This applies to everything, BTW, even to Scheme, ML, Java and TLA+ -- all of which I really like. I can rarely if ever bring myself to believe that some approach to software is universally (or close to it) better than others, unless there is some very compelling evidence.

> Do you know the precise time in the video?

No. I remember Leroy mentioning it at the very beginning, and then they discuss it at some later point, as well.