Has anyone working with Elixir used TLA+ to model their code? It seems as if it’d be a very natural fit and I am curious if anyone has any feedback on that combination.
But never had the desire to try within Elixir.
So I’m also curious if anyone does?
I guess there are two of us interested in the topic. I’ve been tweeting with @QuinnWilton on the subject.
I haven’t yet but Hillel Wayne’s Twitter feed is full of bits and bobs about formal verification, as is his blog. I’m frequently tempted, and if I ever contribute to serious distributed-systems work again I will probably dabble a little. IIRC Quinn used Alloy recently rather than TLA, though?
There’s also Quickstrom as a very recent release that is frontend-focused but quite interesting.
Ah–thanks for the pointer Shane!
I am not, but this an area that I am interested in! Just haven’t had enough time to dig into it yet.
I’m in the same boat, definitely a field I’m interested in but never had the use-case where I thought: now I’m gonna dig in!
I am interested in this subject.
have anyone try this library tla-transmutation before?