Re: [tlaplus] Spec Review Request

[Jamie White <ja...@xxxxxxxxxxxxx>]

Hi Chris

Thank you so much for your message. It’s a treasure trove of knowledge and valuable advice.

Your assumptions are pretty much spot on, but allow me to clarify the intent a little further:

The spec in its current state is meant to capture the essence of the system, in order to then demonstrate the process of specifying safety and liveness properties, and finding bugs with TLC.

My idea is that I can sit down with other Herokai who’ve not yet seen TLA+/TLC in action, and work through adding invariants such as “the playhead should never jump backwards” or “a race of skip messages should not cause the server to miss out tracks”. No doubt there are other invariants I’ve yet to think of that my colleagues will suggest right away.

So it’s a sort of “jumping off point” for demonstrating the practical applications of TLA+ to the folks here.

Modelling duplicated and reordered messages would indeed be an interesting extension. In its current environment, we get some guarantees of atomicity from the underlying tools (Phoenix/Elixir/Erlang) but questioning those assumptions (and our understanding of those assumptions) would be a good exercise.

Finally, I’ll confess that though this is the first spec I’ve written, I have read through a good chunk of Specifying Systems and avidly followed the video course… so i can’t claim to have learnt TLA+ in the space of a week :)

Thanks again. I’ll keep y’all updated on Heroku’s usage of TLA+.