[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Possible new language constructs for TLA+3?

It's easy to find useful things to add to a language.  I expect if I asked 100 TLA+ users, I could get 10 reasonable suggestions.  And any single addition adds little in the way of mental burden.  It requires ruthless discipline to keep the sum of those little additions from becoming burdensome.  All the constant operators appear in Tables 1 and 2 of "Specifying Systems".  There are already too many of them, as evidenced by Andrew being unaware of "EXCEPT ![a][b]". 

I remember many years ago listening to a talk in which someone described a project that led them to propose additions to the TLA logic.  I remarked that they had spent 6 months adding things to TLA that it had taken me 15 years to learn how to get rid of.

I suggest that instead of thinking of things to add to TLA+, it would be much more useful (and much harder) to come up with things that can be removed.  I'd love to see temporal logic removed, but I don't know anything better to replace it with.


On Monday, April 9, 2018 at 4:11:38 AM UTC-7, Ron Pressler wrote:

Can you elaborate some more on the motivation? Minimalism is certainly a virtue, but surely something can be said for convenience of reading. Syntax sugar doesn't add new concepts, so it adds little in the way of a mental burden (and it can be desugared from the AST by the parser, keeping tools simple), and IF it is intuitive it can assist with readability. Free tuples are a great example. Not only is the syntax intuitive, but it is so in line with ordinary mathematical notation that even if not taught, users may guess it is supported and try it.

Using a LET to simplify nested comprehensions requires the spec writer to name some intermediary set that may not be meaningful on its own, and requires the reader to at least read the name and maybe ponder its significance. It's not a show-stopper, but it does add some small mental road-bump.

As to standard modules, I can think of some more reasons. By given common idioms standard names they can make it easier to read other people's specs without studying their definitions. They can also ensure that the definitions are correct. Finally, they can then serve as a common ground for reusable theorem modules. Obviously, it's not a good idea that have the standard modules contain any possibly useful definition, but some very common idioms could be added. For example, I think many definitions in the standard TLAPS modules may be candidates.