Prototyping fun new TLA+ syntax

[Andrew Helwer]

At the TLA+ community event I gave a talk where I suggested one of the things we could look at doing is simplifying TLA+ syntax. And - to be clear, none of this serious or committing, we're just playing around to see how it looks - Hillel Wayne had some fun ideas to make the logical operator syntax look more programmerish. So I whipped up some changes to SANY and voila - it works and you can try it! TLC even checks it.

https://github.com/ahelwer/tlaplus/pull/4

All the Unicode work along with a bunch of parser testing work funded by the TLA+ Foundation has made it quite easy to make simple changes to the parser. So I'm taking requests! Have any fun syntax ideas? I'll try to implement them for you, assuming they aren't too involved.

It's one thing to speculate about how syntax could look but this will let you try it out!

Andrew Helwer

[Andrew Helwer]

(some clarification!) The foundation isn't funding me to work on this, it's just for fun on my own time; actual changes to the language or tools that get upstreamed have to go through the RFC process and be approved by a body called the Specification Language Committee (SLC). I'll let the SLC themselves speak to their priorities for the language, although believe it is largely guided by the document The Future of TLA+ [pdf]. So to reiterate - this is just playing around and experimenting with different looks!

Andrew Helwer