December 2024 Monthly Development Update
Hello! +You’re reading the inaugural edition of the TLA⁺ Foundation monthly development update. +Here I’ll summarize the past month of development for the benefit of Foundation patrons and interested members of the community. +These posts are authored by Andrew Helwer and while I’ll focus a fair bit on my own work (as a way of providing a monthly status update to the Foundation, really), I will also provide a rundown of other happenings in the community! +If I missed your contribution or there was some important part of it I didn’t capture in the summary, worry not! +These newsletters will be published monthly so it’s easy to hop on the next train; try opening an issue here.
If you’re interested in getting involved in the TLA⁺ community:
- Learn TLA⁺ starting here!
- Read the mailing list here!
- Join the monthly virtual community meetings here!
- Start hacking on the tools themselves here!
Let’s start with some interesting non-coding-related developments & announcements:
- Leslie Lamport published a new book, titled A Science of Concurrent Programs! +It’s freely available for download but a physical edition is in the works. +I’ve been reading & enjoying it and asking lots of questions on the mailing list. +It’s very much focused on the “TLA” part of TLA⁺ (meaning the Temporal Logic of Actions) so it’s a good read if you want to go really in-depth on the logical theory underpinning the TLA⁺ language.
- The TLA⁺ Community Event 2025 was announced, to be co-located with ETAPS 2025 in Hamilton, Ontario, Canada on May 4th, 2025. +We hope to see you there! +The talk proposal submission deadline is February 7th, 2025.
- East of the Atlantic, ABZ 2025 - the 11th International Conference on Rigorous State-Based Methods - will take place from June 10th to 13th of 2025 in Düsseldorf, Germany. +TLA⁺-related papers are welcome; the deadline for submitting abstracts is February 3rd, 2025.
- Jack Vanlighty wrote a blog post on using TLA⁺ to obtain statistical properties of distributed system designs.
- Lorin Hochstein has been on a TLA⁺ blogging tear, publishing three excellent blog posts in quick succession: Specifying serializability in TLA⁺, Multi-version concurrency control in TLA⁺, and Extending MVCC to be serializable, in TLA⁺. +The first post is especially effective as an introduction to using refinement to express whole-system safety properties that just can’t be done with single-state formulas.
- At the November virtual community meeting, Feng Wenhan presented his work using the TLC state graph export function to drive model-based testing; some shortfalls in the state graph export functionality led to the proposal of designing a robust state graph export format.
- Also at the November virtual community meeting, Leslie Lamport announced his retirement at the end of the year at the age of 83. +A well-earned rest, although his contributions will be missed!
Now on to coding-related community developments:
- Federico Ponzi is prototyping a TLA⁺ Formatter, including hammering down the default settings. +If you have opinions on how TLA⁺ should look, now is a great time to weigh in!
- Julia Ferraioli updated the TLA⁺ Foundation website with blogging capabilities, facilitating the very post you are reading right now! She chose the Hugo static site generator, of which I am also a fan.
- William Schultz released Scimitar, a tool for verifying the safety of distributed protocols based on the technique of inductive proof decomposition in TLA⁺.
- Hillel Wayne has started contributing to the TLA⁺ VS Code plugin, adding some nice diagnostic messages for PlusCal.
- Ioannis Filippidis landed some long-awaited changes adding support for bound tuple quantification to the TLA⁺ Proof Manager (TLAPM), reviewed by Damien Doligez.
+This enables TLAPM to parse quantification expressions that use tuple destructuring, like
∀ ⟨x, y⟩ ∈ ℕ × ℕ : x + y ∈ ℕ. - We welcomed Mathieu Borderé as a new contributor as he landed his first PR in the TLA⁺ tools, improving command line help output for the parser!
- Longtime TLA⁺ Tools maintainer Markus Kuppe submitted many changes, focused on the TLA⁺ debugger (1, 2), miscellaneous bugfixes (1, 2, 3, 4, 5, 6, 7, 8), and some design-level work on shortening & choosing counterexample traces (1, 2).
- Finn Hackett found an issue with TLC where reading non-ASCII strings from disk causes a crash; a fix is pending review.
Finally, things I worked on over the past month-and-a-half - all funded by the TLA⁺ Foundation:
- I adapted the TLA⁺ syntax test corpus for use on TLAPM, which implements its own TLA⁺ parser in OCaml. +These found a number of issues in the parser, and also resulted in me writing around fifty additional syntax tests which were backported to the TLA⁺ Java-based tools and the tree-sitter-tlaplus grammar.
- I investigated transitioning TLAPM’s parser to use SANY, the Java-based TLA⁺ tools’ parser. +SANY has an XML parse tree exporter which would avoid any FFI weirdness between OCaml and Java code. +I submitted some fixes (1, 2, 3) to dust off the XML exporter and wrote a prototype consumer in OCaml for the XML output. +After poking at the prospect of translating SANY’s parse tree output to TLAPM’s internal parse tree format for a couple of weeks, I’m thinking the project has a fairly high risk of dragging on without any intermediate milestones to lock in value. +It remains to be seen whether the TLA⁺ Foundation will commit to it. +I think there are some work possibilities that could smooth the way, for example by developing a large corpus of tests for SANY’s semantic- and level-checkers to build familiarity with their workings.
- I played at stepping into the TLAPM maintainer role, just making changes to the development infrastructure like fixing a flaky CI build, adding developer documentation, hunting for ways to cut down the release size, and - most substantially - setting up rolling pre-releases for TLAPM! +TLAPM hasn’t seen an official numbered release for a couple of years now, so most people seem to build it from source to get the latest changes; this work just makes the built artifacts from the head of the main branch easily available for download.
- I submitted a few one-off bugfixes and enhancements for the Java-based TLA⁺ tools: some tests and fixes for the level-checker, and the removal of a now-unused error logging path in the parser.
- I wrote up a proposal for additional TLA⁺ standardization that has been rolling around my head for a bit, on standardizing human-readable error codes similar to Rust and C# and many other languages. +I think the benefits would be wonderful, especially with regard to stimulating test coverage off the happy path.
Newbie Corner
Quite a bit of stuff going on in TLA⁺ development! +Don’t be intimidated though, there is plenty of room and desire for newcomers. +Join the mailing list and monthly community meeting to introduce yourself if you’d like to join in!
Here I will highlight one issue each month that I think would be good for new contributors. +This month it’s the inability of the TLA⁺ parser to handle backticks in strings. +The primary reason this is a good first issue is that the required change seems very localized and tremendously unlikely to introduce any bugs; the second reason is that it’s in a very well-tested part of the codebase (the syntax parser), which has the standard TLA⁺ syntax test corpus levied against it - a corpus you will contribute to as part of the fix! +I hope to see somebody pick this up in December!