> Absolutely, and thus types and specification via TLA+ are not in opposition. In fact they can work in harmony.

Sure, it's just that TLA+ can open your mind to the idea that you may not need types for things you think you do -- even in a programming language. It can also show you how you can do mutation and still remain pure without using monads or any higher-order function composition. This idea is used in synchronous programming languages, too, so this is something that definitely applies to programming languages.

> Indeed, even the fundamental TLA+ notion of "priming" variables seems that it would immediately be an impediment to composability.

Why? It's a perfectly pure operator and it distributes. Op(x, y)' = Op(x', y'), assuming Op doesn't have any other variables in it, i.e., it's a "level 0" operator.

> Correctness does compose in my experience as a mathematician

I can show you a trivial example of why that's not true: the gravity equation. Everything composes, yet two instances are already chaotic. You can't extrapolate almost anything you know about the gravity equation to predict the bodies' positions over two instances. For discrete processes, such chaotic behavior is small potatoes. We don't even use the word "chaotic" because we're way beyond that. The problem is this: if everything is simple, you can compose correctness. But when everything is simple, composition isn't really required. This is what I'd like to call the "FP extrapolation problem". FP works beautifully for simple examples, i.e., where new approaches don't really matter. People then extrapolate from toy examples and assume it can scale (in spite of the theory that says otherwise), yet no one has yet shown that it does in practice. By that I don't mean that you can't write large programs in FP. Of course you can. But the advantages that are very clear in the simple cases (where they don't matter), start dissipating and you just don't see a drastic effect at scale (maybe the effect is even negative; nobody knows).

> Please explain your terminology.

Sorry, I meant a TM that terminates eventually. I think that's either the current record or the lower bound. Don't remember.

> I find this a very puzzling statement. States in subcomponents can be easily hidden in every common-or-garden programming language.

They're hidden from the programmer's view, not from their effect on correctness. That is precisely the result that says that verification isn't fixed-parameter tractable. Namely, if the cost of verification is O(|S|) when S is your number of states, you can't say, well, each of my components has n states and I verified them individually, and now I want to compose k components, and so the cost of verification would be O(small function of k). It will be O(n^k) or something like that.

> Sure, but as we've observed, it doesn't actually tell you anything about the final implementation you come to write.

Right, but nothing else can, either, unless you do end-to-end verification, which is far beyond what 99.9% of projects can afford to do (or need to). Here is where you rely on software engineering practices, tests and whatever tools you have for local properties that help prevent easy bugs (like types and static analysis). There is nothing that can help you prove interesting logical properties at this level, at anything close to an acceptable cost.

> What does it mean to you?

Oh, the same. It just doesn't look the same way in TLA+, where you compose things as A ∧ B rather than A(B) (they don't mean the same thing).

> What exactly does that mean?

Alright, let me try: suppose you have a higher-order function, say `filter`, that takes a function of type `a -> bool` (where a is a type parameter), and filters a list. Now suppose you want to prove that, say, the length of the resulting list is no bigger than the input list. In a functional language you say, I have a function parameter `p` that could be anything of the appropriate type `a -> bool`. In TLA+ you don't need this because you can say that p is not a parameter of a certain type, but a concrete, specific program that nondeterministically returns either TRUE or FALSE. You prove your theorem for that specific p, but it really covers the same as all predicates p of that type.

The cool thing, then, is this: you can ask, what is the relationship between that nondeterministic program p, and a deterministic program p1, that, say, returns true iff its argument is an even number? Well, it's a refinement relation (any behavior of p1 is a behavior of p, but not vice-versa), and in TLA+ this is expressed simply as p1 => p, where => isn't some special notation but the same-old familiar implication operator from propositional calculus, because in TLA+, a program is a binary boolean predicate that evaluates to TRUE iff there's a next-state relation between its two input states, the unprimed and primed.

The key to that is understanding the model (in the logical sense) of a TLA formula (i.e. a program). The model is a set of all possible behaviors, where a behavior is a sequence of states (similar, but not exactly a trace in the process-calculi sense). So a program is a set of behaviors. A program property (i.e., the program never sends the character "x" over the network), or a "type", is the set of programs that satisfy it (I mean by the simple isomorphism between predicates and sets). Here is the crucial bit: as the TLA logic only allows to specify properties that must be true for all behaviors or none (hence the problem with probabilistic algorithms), there is no need to keep the behavior sets for each program in the "set of programs" separated, and instead of a set of programs -- i.e. a set of sets of behaviors -- a program property can simply be a set of behaviors. But a set of behaviors is a program! Therefore a program property, or a "type", in TLA is the same thing as a program. Program properties and actual algorithm specifications become a hierarchy of nondeterministic programs that refine or abstract one another. So the program that does parallel merge-sort is a refinement of a program that does some sort of merge sort, and that, in turn is a refinement of a program that "sorts somehow". And all those relationships are simple propositional calculus connectives, and you can reason about what kind of low-level steps a low-level specification does for each abstract step in a higher level specification.