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

[tlaplus] Some blog posts I wrote about TLA+

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

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 on the web visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUVy71Tv2G%2BuWiqn%2B6VrZmxH8bF%3D642z4LNrZmMdqTiJ8A%40mail.gmail.com.