Some blog posts I wrote about TLA+

[Andrew Helwer]

Here are two posts I published recently about TLA+:

Pseudocode Showdown: Python vs. PlusCal & TLA⁺

I look at how well PlusCal works as a pseudocode replacement, taking the case study of a string algorithm paper published in 1980 that contained bugs in its pseudocode. It was for this post that I was spamming up this group last week with questions about proofs. I didn't end up writing a proof for this algorithm because I figured it was extremely complicated and would have taken about two weeks, but I'm glad I finally learned how to write TLA⁺ proofs (it's been a goal for nearly a decade!). I also compared the TLA⁺ proof language to the Lean proof language. I wonder how much of the Lean user experience could be transferred to the TLA⁺ proof language UX.

Using TLA⁺ at Work: Designing a Snapshot Coordination System

Report about an experience with TLA⁺ use on the Microsoft Azure DNS team, with a now-open-sourced spec. The model checker found an interesting 12-step error trace in the proposed design. It also talks about the experience of implementing actual code following a TLA⁺ spec.

Hope you enjoy!

Andrew Helwer