3 ms·
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
by hwayne 2y ago
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.
- setheron 2y agoSo for us normies does that mean skip TLA?
- hwayne 2y agoNone of the replacements I've seen so far are mature enough for me to recommend them over TLA+.
- igornotarobot 2y agoI 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.