The Future of TLA+

[Leslie Lamport]

The future of TLA+ is now in the hands of the TLA+ Foundation.   The document The Future of TLA+ has been written to serve as a guide to how proposals to change the language and related parts of the TLA+ infrastructure such as PlusCal should be viewed.

Leslie

[Hillel Wayne]

I didn't see the tables in the document and didn't immediately realize that they were supposed to be in Specifying Systems. Maybe each table could be given a page reference?

H

On 8/28/2024 6:58 AM, Leslie Lamport wrote:

The future of TLA+ is now in the hands of the TLA+ Foundation.   The document The Future of TLA+ has been written to serve as a guide to how proposals to change the language and related parts of the TLA+ infrastructure such as PlusCal should be viewed.

Leslie

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/189790eb-98a3-4569-a22e-87147f23b791n%40googlegroups.com.

[Hillel Wayne]

> Another possible candidate for removal is the notation for binary, octal, and hexadecimal numbers—such as \O22, which is usually written 22_8 and equals 18. Again, we don’t know if its use is rare enough.

We can get a rough estimate by using GitHub code search. It won't surface private uses but there are at approximately 5000 TLA+ specs on Github (including duplicates). I ran the following searches:

• `path:*.tla /\\h\d/ NOT is:fork`: 3 results, all files testing the `\h` feature.
• `path:*.tla /\\h\d/ NOT is:fork`: same 3 test files.
• `path:*.tla /\\b\d/ NOT is:fork`: ditto

H