IMO TLA+ is not very good. It has super weird syntax, and a whole separate DSL (PlusCal) to give it workable syntax for programs. You can really tell it was created by the same mind as LaTeX.
What is the Typst of formal modeling?
Another issue is that you end up with a formal model that passes, but then you have still have to convert that to a real language by hand and not make any mistakes.
I like how PlusCal looks, however I vouch for the same sentiment as you.
As already expressed multiple times, if it isn't like Dafny, Lean, FStar, SPARK, Frama-C, possibly others, where the formal model can be directly mapped to code, I don't see what was actually proven, other than a theoretical exercise.
Many TLA+ users will tell you the greatest value of writing a spec was it forced them to think clearly about their system. However, thinking is very hard to sell, so we tend to center the razzle-dazzle about model-checking properties of your state space. Which is a great capability, don't get me wrong! Most non-trivial systems have a state space far larger than can be assessed for finding bugs via thinking.
IshKebab · · focus · HN ↗
What is the Typst of formal modeling?
Another issue is that you end up with a formal model that passes, but then you have still have to convert that to a real language by hand and not make any mistakes.
pjmlp · · focus · HN ↗
As already expressed multiple times, if it isn't like Dafny, Lean, FStar, SPARK, Frama-C, possibly others, where the formal model can be directly mapped to code, I don't see what was actually proven, other than a theoretical exercise.
ahelwer · · focus · HN ↗