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.
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.
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.
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.