3 ms·

Thanks! If there is an utility to this post other than just as an exercise in using Z3Py, it isn't just getting TLA+ into Z3 which as you say is already covered

Thanks! If there is an utility to this post other than just as an exercise in using Z3Py, it isn't just getting TLA+ into Z3 which as you say is already covered by the apalache project. I think that as someone who doesn't really know TLA+, but is very familiar with python, it feels very comforting to being using python instead of something totally foreign. Also since it is such a small translation (really the 10 lines always combinator is the core of it), if you want/need access to the logical guts of the checker, it's easy. Or if you wanted to autogenerate a spec in some manner, being embedded in python is a huge boon.

pron 6y ago
TBH, this is a point I struggle with. TLA+ is different from programming languages because TLA+ is a language for writing mathematics [1] and mathematics is different from programming. Internalising that -- and learning how to describe things with mathematics -- is the challenge, not learning new syntax. In fact, I think that anything that makes simple mathematics look superficially similar to programming makes learning TLA+ more difficult, not less. But either way, once you've learned how to use mathematics to describe systems, wouldn't you rather use syntax that's as close to standard mathematical notation as possible? If physicists and engineers use standard mathematical notation to write mathematics even when describing the behaviour of some, say, spring system, why would programmers want to use a special notation when writing mathematics? Don't get me wrong -- I think it's cool to show how to express TLA+ with Z3's Python API, perhaps it even helps some people understand what TLA+ formulas mean, but I disagree that it makes using TLA easier. I realise this is a matter of pedagogy, and preference might be individual, but that's my point of view. P.S. This is beside the point, but I've been programming for ~30 years, and while I've programmed professionally in quite a few languages (more than ten), I don't know Python (or JavaScript; at least not well). Neither do most programmers I work with. There's no doubt Python is among the best known programming languages, and millions of programmers know it, but many more than you might expect don't (just as I was surprised to realise there are programmers who don't know C or Java)! IMO, TLA+ is easier to learn, at least as far as syntax and core modules go, than any programming language. [1]: https://old.reddit.com/r/tlaplus/comments/enencr/yet_another_example_that_tla_is_math_not/ https://old.reddit.com/r/tlaplus/comments/enencr/yet_another...
- philzook 6y ago
  I'm on board for there being a problem with conflating programming languages with things that are not. This was a revelation for me for example with Verilog, which almost has the trappings of an ordinary programming language but is not. It is better conceived of as a DSL for digital circuit diagrams. And I do not think of TLA+ as a programming language. I really used python here as a scripting metalanguage for constructing "TLA+" terms and orchestrating calling the checker, which to my knowledge does not have an analog in the standard TLA+ toolset. In fact one might use python for such a task, writing TLA+ and config files and shelling out to the checker. It is however usually the case that I find myself annoyed when someone hands me a sandboxed DSL with its own syntax. Most DSLs do not get enough developer resources to become extremely feature complete. Embedding the DSL makes it much easier to extend the capabilities in ways the designer didn't imagine. When doing things by hand scientists and engineers use ordinary mathematical notation, but when doing scientific computation they use programming languages. I myself have a physics background and was strongly paper and pencil oriented for years and am now much heavier in the programming side of things. There are insights to be had from both perspectives. The programming/simulation side of a scientific theory is nearly necessary for me to be convinced you're not talking total nonsense. Without a calculating angle, a declarative syntax has little teeth. The precision required by programming makes it difficult to dream and sketch though. Things have to be half built before they're built.

pron 6y ago

TBH, this is a point I struggle with. TLA+ is different from programming languages because TLA+ is a language for writing mathematics [1] and mathematics is different from programming. Internalising that -- and learning how to describe things with mathematics -- is the challenge, not learning new syntax. In fact, I think that anything that makes simple mathematics look superficially similar to programming makes learning TLA+ more difficult, not less. But either way, once you've learned how to use mathematics to describe systems, wouldn't you rather use syntax that's as close to standard mathematical notation as possible? If physicists and engineers use standard mathematical notation to write mathematics even when describing the behaviour of some, say, spring system, why would programmers want to use a special notation when writing mathematics? Don't get me wrong -- I think it's cool to show how to express TLA+ with Z3's Python API, perhaps it even helps some people understand what TLA+ formulas mean, but I disagree that it makes using TLA easier. I realise this is a matter of pedagogy, and preference might be individual, but that's my point of view. P.S. This is beside the point, but I've been programming for ~30 years, and while I've programmed professionally in quite a few languages (more than ten), I don't know Python (or JavaScript; at least not well). Neither do most programmers I work with. There's no doubt Python is among the best known programming languages, and millions of programmers know it, but many more than you might expect don't (just as I was surprised to realise there are programmers who don't know C or Java)! IMO, TLA+ is easier to learn, at least as far as syntax and core modules go, than any programming language. [1]: https://old.reddit.com/r/tlaplus/comments/enencr/yet_another_example_that_tla_is_math_not/ https://old.reddit.com/r/tlaplus/comments/enencr/yet_another...

philzook 6y ago
I'm on board for there being a problem with conflating programming languages with things that are not. This was a revelation for me for example with Verilog, which almost has the trappings of an ordinary programming language but is not. It is better conceived of as a DSL for digital circuit diagrams. And I do not think of TLA+ as a programming language. I really used python here as a scripting metalanguage for constructing "TLA+" terms and orchestrating calling the checker, which to my knowledge does not have an analog in the standard TLA+ toolset. In fact one might use python for such a task, writing TLA+ and config files and shelling out to the checker. It is however usually the case that I find myself annoyed when someone hands me a sandboxed DSL with its own syntax. Most DSLs do not get enough developer resources to become extremely feature complete. Embedding the DSL makes it much easier to extend the capabilities in ways the designer didn't imagine. When doing things by hand scientists and engineers use ordinary mathematical notation, but when doing scientific computation they use programming languages. I myself have a physics background and was strongly paper and pencil oriented for years and am now much heavier in the programming side of things. There are insights to be had from both perspectives. The programming/simulation side of a scientific theory is nearly necessary for me to be convinced you're not talking total nonsense. Without a calculating angle, a declarative syntax has little teeth. The precision required by programming makes it difficult to dream and sketch though. Things have to be half built before they're built.