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.
The closest thing I’ve come across to this is Z (“Zed”) notation. It’s from the late 70s, quite influential and pretty easy to read with a bit of logic symbolism. The same designer (Jean-Raymond Abrial) and colleagues also made the B method which can also do program refinement. Several other “well-known” (relative to other formal methods) formal specification systems were influenced by Z, including possibly TLA+ as I’ve read somewhere (but cannot confirm). Z and B both have free tooling available online.
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.
NooneAtAll3 · · focus · HN ↗
better question is "what's the markdown of formal modeling?"
the best outcome for everyone is to have something that's so easy it's ubiquitous
Revanche1367 · · focus · HN ↗