Hacker News Reader

Comment by aychtang | Hacker News Reader

TLA+ was created so you can quickly model / specify a design, check it works under your assumed invariants and maybe explore alternatives up front, giving you a plan for how your system should work in theory.

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.

View on HN

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

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.

I think that's fair. It's been described elsewhere as 'exhaustively testable pseudocode'.

Reply on news.ycombinator.com