I'm very much hoping this will be the case!
> > 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.
That's not an assumption I want to have to make! Since I don't understand this specific example perhaps my challenge here is unwarranted, but in general if I have to "assume" anything then that's an impediment to composability.
> 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
OK, I think I see. You prove something using the specific, concrete p which has fewer properties than any other p, so therefore anything that holds for it must hold for the other p too. I don't quite see how this is different from proving it for "arbitrary p" but perhaps it will be come clear as I learn more.
> I mean by the simple isomorphism between predicates and sets
And this is why I get worried about TLA+ using "simple mathematics". This "simple isomorphism" simply doesn't exist, as I'm sure you know. You have to restrict yourself to saying "simple isomorphism between predicates on a set and subsets of that set", at which point I start to worry that any higher-order possibilities go out of the window.
> But a set of behaviors is a program! Therefore a program property, or a "type", in TLA is the same thing as a program.
Sure, but a possibly nondeterministic one that you can't actually implement (at least not directly).
Anyway, thanks for the introduction. When I get some time I will look into it further.
You don't need to make that assumption, though. TLA+ checks it for you. My point is that everything is pure and well-behaved. The very same issues of modality happens when you use monads. Only in TLA+ it's very simple to see when an operator is a constant (called level 0), a state function/predicate, i.e., a function of the current state (level 1), an action/step (level 2), or a full temporal formula (level 4). In a temporal formula, you can say something like, whenever my program sees an event x, it would eventually output a response y. In a way, TLA+ has 4 syntactic types, and the relationship between them is checked instantly at parsing. E.g. you can't take an action or a temporal formula and prime it (TLA+ checks "inside" your formula and knows what level it is). Priming a constant keeps it a constant; priming a state function turns it into an action (a relationship between two states).
> This "simple isomorphism" simply doesn't exist
No, I meant something very simple. Any boolean predicate, e.g. "this number is even", is the same as the set of all even numbers. It's a characteristic function. It always exists.
> Sure, but a possibly nondeterministic one that you can't actually implement (at least not directly).
Right, but nat -> bool, is the same as saying "all programs that take a natural and return a boolean", which is the same as the ND program that for any natural nondeterministically returns true or false. It's describing the same set or type, but in a different way, which makes simple logical implication the same as subtyping or type inhabitance. B is a subtype of A, is, in TLA+, B => A. a is an instance of A, is in TLA, a => A.
BTW, it's not true that TLA+ can't tell you that your implementation is correct. It can, it's just hard (but probably no harder than in Coq). What you do is, you write a high-level model and prove it. Then you implement it in a programming language, and you write a compiler from that language to TLA+. Then you check that the TLA+ version of your implementation is a refinement of your high-level model. Academic teams have done this for C and Java. The problem is that implementations have many details, so it doesn't scale beyond small programs.
> When I get some time I will look into it further.
I'd say that the effort to learn TLA+ is comparable to learning a very simple programming language with a couple of deep concepts. Scheme maybe. It takes two weeks to be able to write large, complex specifications (though probably longer for the theory to become intuitive). The entire documentation for all the "standard libraries" fits on a single page. The reference for all the language, with full explanations, fits on 4 pages. This is all of TLA+, including the standard library, minus the proof language, including all syntax sugar: http://research.microsoft.com/en-us/um/people/lamport/tla/su... (e.g. all the special syntax for sequences and records is just sugar for functions, so r.f is sugar for as r["f"]). Personally, I'm interested in theory for intellectual reasons, but the single reason I picked TLA+ is that Amazon technical report, where they showed that 1. learning it is easy for engineers to do on their own, and 2. it scales well for very large systems.