Hacker News Reader

I wouldn't say it's a TLA+ alternative because it cannot do the most powerful and useful things TLA+ does (esp. refinement), but it is an alternative for programmers who just want to specify at a level that closer to code and model-check specifications.

View on HN

Every time I see a new TLA+ replacement my first thought is "Oooh this will be good for the 99% of normal stuff people do with TLA+."

Then I look through some of the specs I've written with clients and find the one absolutely insane thing I did in TLA+ that would be impossible in that replacement.

Shoutout to operator labels.

So for us normies does that mean skip TLA?

None of the replacements I've seen so far are mature enough for me to recommend them over TLA+.

I believe this is really the tragedy of formal verification tools. Everybody wants a tool as robust as a compiler. At the same time, nobody wants to invest into development of such tools. Microsoft Research 20 years ago was probably an exception to that. The other companies wish to immediately hide these tools and the benchmarks behind the IP and closed source. As a result, we have early stage MVPs that are developed by 1-3 people.

Reply on news.ycombinator.com