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.

I did quite a lot in JavaScript based on → sam.js.org 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.

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?

I’m not sure what you mean by “update”? If you’re interested in trying to use TLA+ in conjunction with Elixir it’s sort of DIY and I don’t think that will change any time soon given that TLA+ only builds models not code.

Elixir Programming Language Forum

TLA+ With Elixir

Questions & Help Questions

Onor.io September 3, 2020, 4:09pm 6

Ah–thanks for the pointer Shane!