What TLA+ can and can't check
29 points by hwayne
29 points by hwayne
You can definitely see that some things are more ergonomic to express in TLA+ than others; like my reachability properties post was indeed unhinged! I've been using TLA+ for more than a decade, have been paid to work on the core tools, and am probably in like the top 5-10 people worldwide for TLA+ knowledge - and I still didn't understand how to express reachability until writing that blog post the other day. So I do think it is valid to say some things can be technically expressed but are definitely not ergonomic.
I wonder whether this is inherent to the formalism, or maybe the formalism can be extended to make these ergonomic, or by doing so we fall afoul of the same age-old branching-time vs. linear-time logic debate that has been raging (or at least gently warming) since Arthur Prior (in an excellent example of nominative determinism) came up with temporal logic in the 1950s. At very least TLC could be easily extended to check basic reachability properties, but not in a way where they could be composed with other properties.
CTL* can supposedly check both reachability and liveness, but I haven't seen any tools based on CTL* and wonder what the catch is.
The weird thing I've heard about CTL* is it somehow encodes both branching- and linear-time logic, but beyond that I did find this weird 2002 paper I'd not previously heard of called Branching vs. Linear Time: Final Showdown.
Honestly this was really great, a nice concise run down of what can be expressed.
I think I’d like a dictionary of the other kinds of properties that are expressible in other formalisms as a guide to thinking about what to specify even if there isn’t a ready-made checker to hand. In that way I think it would help the reader (me) reason about code and write tests to attempt to check (or disprove) those properties.