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, wh

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.