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.
8 Likes
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.
1 Like
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.
4 Likes
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!
2 Likes
IS there any update?
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.
2 Likes
I want to carry out testing for GitHub - archethic-foundation/archethic-node: Official Archethic Blockchain node, written in Elixir.
A public blockchain, I am looking to test Gen-state machines for custom consensus, as there are too many flow/situations to handle.
What will you all, will recommend to me?
