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

[tlaplus] Re: Prototyping fun new TLA+ syntax



(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

On Mon, May 19, 2025 at 9:49 PM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
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


--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUWB%2B748utFo5FM1%2BPBDVUCFKvGs9GL7h2G%3DWiZ-tnTDfA%40mail.gmail.com.