> I have no disagreement with what FL writes. However, saying "TLA+ is
> hard, but it's good for you" will needlessly scare away students.
I apologize. I definitely don't want to frighten students. I swear I don't.
> Students need to learn to think of
> programs as specifying an initial states and next-state relations.
> they use describe a program in terms of an initial predicate and
> next-state relation.
Well that's true: this is the most important idea in TLA+.
--
FL