Hacker News Reader

How does TLA compare to Spin?

The main difference is that I know how to write TLA+ and don't know how to write Spin

I have the Spin book and intend to read it, but I keep having other stuff come up. It's mocking me, I know

The Spin book, the one with the parrot on the front, is actually pretty good. Maybe not for someone like you with deep expertise, but for almost anyone else, it has a mix of motivating anecdotes, examples, computer science and insights that I've not seen bundled up anywhere else.

Your advocacy for TLA+ makes me want to try it out. I just wanted to understand what I might be getting into.

I used Spin a few years back, so my memory is a bit hazy, but I remember Promela (Spin's modeling language) feeling extremely low-level in comparison. It felt a bit like more limited C with non-deterministic choice stuck in there. TLA is a first-order logic language, and the tooling (while not great by modern language standards) felt more pleasant than Spin.

It could be that you get faster model checking with Spin though, I'm not aware of any comparisons.

Reply on news.ycombinator.com