Hello, > Le 12 avr. 2026 à 09:57, Irwansyah Irwansyah <irwansyah@xxxxxxxxx> a écrit : > > Unfortunately, the whole point of using TLA+ is we can go straight forward attacking the problem without having to deal with setting up developnent environment that came with progrramming languages I understand, and don't question that. TLX reads and emits TLA+ and PlusCal, and calls TLC. Its DSL is based on TLA+. I'm not reinventing the wheel, and don't intend to: I am neither a formal specs expert nor a mathematician. That said, even though I have a long experience with Perl, LaTeX, XSLT, and a bit of Erlang, I found the syntax (not the concepts) of TLA+ and PlusCal, well... much more intimidating 😅 I also have experience with Smalltalk, Python and Elixir, so I understand the importance of Developer Experience -- DX. Thus, with TLX, I just tried to improve the TLA+ DX (it worked for me), make formal specs usage frictionless in Elixir projects (it worked in my project), prove a large, distributed, Elixir project design and implementation were correct (TLC found one bug and one design ambiguity, so it worked for me), and integrate formal specs verifications into CI (it worked ! 🥳). So, I tried to make TLX a good citizen in the TLA+ ecosystem. And simply decided to open source it. That's all. Thanks for your feedback 🙂 Georges -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion visit https://groups.google.com/d/msgid/tlaplus/BB88B7B6-F487-4701-BC89-1AAE241B3E5A%40gmail.com.
Attachment:
signature.asc
Description: Message signed with OpenPGP