4 ms·
We're seeing more people create DSLs that compile to TLA+. For example, salt lets you write TLA+ specs in Clojure: https://github.com/Viasat/salt https://github
by hwayne 6y ago
We're seeing more people create DSLs that compile to TLA+. For example, salt lets you write TLA+ specs in Clojure: https://github.com/Viasat/salt https://github.com/Viasat/salt
- elcapitan 6y agoThat's interesting, are there more examples of such languages?
- hwayne 6y agoThe other one I know about is PGo, which is a bidirectional go-pluscal compiler: https://github.com/UBC-NSS/pgo https://github.com/UBC-NSS/pgo
- michael_j_ward 6y agowow, that feels extremely more approachable. Are there downsides to using that?
- hwayne 6y agoI've never used salt myself so couldn't tell you. From a skim, it looks like they don't have module instantiation? Depending on what you're doing that could be a limitation.
- pron 6y agoI haven't used salt, but the thing to understand is that even when the syntax used is Clojure, the semantics is TLA+'s. So, for example, if you use a Clojure function syntax to define a TLA+ operator, that will not behave like a Clojure function, but like a TLA+ operator, which behaves very differently from Clojure functions. So the symbols on the screen might be more familiar, but their meaning will be different from their meaning in Clojure. I think that is more confusing, which would be a downside, but if you find that more approachable -- great, use that.