Would you say that it's closer to "pseudocode you can use to test process assumptions" than a description of the final structure that a program would have?
Yes apart from it's not pseudocode but mathematical formulas.
Your building blueprints aren't made from bricks and mortar because it would just take way longer and be expensive to experiment with, however with software when designing we often use the same tools as building without thinking of the cost like that.
TLA+ and other lightweight modelling languages allow you to experiment with your design and verify that it works without all the tedium of programming languages and their environments / libraries / compilers etc.
huh, I guess I’m going to have to try it because I just realized that I had a hidden assumption that code was definitionally the lightest way to describe a problem
Re:Learn TLA+ (2018)
by 0x62c1b43e on Sunday February 23, 2020 @03:22PM
(#22399295)
A lot of people use PlusCal, which is basically pseudocode that compiles to TLA+. Depending on what you're modeling, PlusCal or directly writing TLA+ might be a better fit.
Like you mentioned it's the software blueprint, and you go from a blueprint to a building by actually building the thing - TLA+ is not made to codegen your product.