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.
For TLA+-styled model checking, though, there is Quint: <a href="https://quint.sh/docs/why" rel="nofollow">https://quint.sh/docs/why
It's a reasonable question. There are novel things I like about the syntax - like vertically-aligned conjunction & disjunction lists - but I don't really want to defend syntax that still uses all-caps KEYWORDS like it's the COBOL era and makes you use string values for enums. The underlying formalism is, however, amazing for thinking in, and it's used by P, Quint, and FizBee which all to varying degrees paint themselves as TLA+ successor languages.
I agree that spec/implementation conformance checking is also an issue. P has apparently had some success with PObserve for trace validation (checking whether the log of a running system is a valid execution of a P spec) but it is still not a well-known method with these tools in the same way that fuzzing or property-based testing have become. This requires some real product-level thinking to make usable and possibly full ownership of the system execution environment inside a VM or something like that.
I feel like PlusCal and TLA+ operate at a different level. I use PlusCal primarily when what I'm modeling has a lot of sequential "A then B then C..." steps. With PlusCal a program counter is implied and it maps more directly to sequential algorithms.
When I write regular TLA+, it's usually for things that aren't nearly as "order-dependent".
You should look into Quint: <a href="https://github.com/quint-co/quint" rel="nofollow">https://github.com/quint-co/quint. It comes with simple syntax and very good developer tooling. Quint to TLA+ is what Typst is to Latex.
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.
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.
Jtsummers · · focus · HN ↗
I'm not sure there is one, but you can start exploring here:
<a href="https://en.wikipedia.org/wiki/Category:Formal_specification_languages" rel="nofollow">https://en.wikipedia.org/wiki/Category:Formal_specification_...
For TLA+-styled model checking, though, there is Quint: <a href="https://quint.sh/docs/why" rel="nofollow">https://quint.sh/docs/why
ahelwer · · focus · HN ↗
I agree that spec/implementation conformance checking is also an issue. P has apparently had some success with PObserve for trace validation (checking whether the log of a running system is a valid execution of a P spec) but it is still not a well-known method with these tools in the same way that fuzzing or property-based testing have become. This requires some real product-level thinking to make usable and possibly full ownership of the system execution environment inside a VM or something like that.
tombert · · focus · HN ↗
When I write regular TLA+, it's usually for things that aren't nearly as "order-dependent".
beu5a · · focus · HN ↗
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 ↗
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 ↗