Hacker News new | comments | show | ask | jobs | submit login

Outside of distributed systems what is it used for?

I've only ever heard of it's use in the formalization of distributed systems.




You are correct the language really shines when there is concurrency (not necessarily just distributed systems), because validating system invariants with the model-checker is just magical. I've also found the language to hold great value for specifications as such; Dr. Lamport seems to believe that most technical problems just disappear when you precisely identify what it is you want to do, and writing a TLA+ spec is an efficient way of accomplishing that. So, I've found it useful to write specs for solutions to very technical problems simply to clarify my thinking and root out areas of sloppiness.


I concur with both these statements, but would widen the former slightly to say that it helps you think (and then validate your thinking) about any non-trivial state-machine - it doesn't have to be concurrent or distributed.

[Used to work at Microsoft, used TLA+ successfully during product development]


Indeed, TLA+ is mostly known for formalizing and verifying distributed systems and concurrent algorithms. This has a few reasons:

1. Lamport's algorithmic work is in concurrent and distributed algorithms, and as he uses TLA for his own algorithms -- and he's TLA+'s first user -- that's how it's known.

2. Few other general software verification formalisms are able to handle concurrency as easily as TLA, so that is where it shines in comparison. Of course, this is intentional because Lamport designed TLA+ to work well for the kinds of algorithms he's interested in.

3. When engineers write software systems that are too complex or subtle to be obviously correct, and could therefore benefit from formal verification, it is usually the case that a concurrent or distributed algorithm is involved.

Having said that, there is nothing specific about TLA+ that makes it any less suitable for sequential algorithms. If you write one that you think is complicated or subtle enough to require help in reasoning, you could certainly benefit from TLA+.

But if you're interested just in sequential algorithms, you do have more options, like Why3/WhyML, which I think is very nice (although I prefer TLA+). Whether WhyML or TLA+ would be better suited to verify your sequential algorithm depends largely on personal aesthetic preferences, as well as some details of requirements. For example, WhyML can generate OCaml code, while TLA+ can't. On the other hand, TLA+ has both SMT solvers and a model checker, which makes it more likely that you can verify the entire algorithm automatically, while WhyML requires manual proof in Isabelle or Coq for properties the automatic solvers can't verify (I hear they're working on a proof language directly in Why; I hope it's as nice as TLA+'s proof language). Also, TLA+ lets you describe your algorithm at various levels of abstraction, and show that the more detailed ones implement the more abstract ones. WhyML is more focused on the abstraction level of actual program code.


I've personally found it absolutely fantastic for modeling business logic. It's also really good for any kind of concurrent system, which covers pretty much every webtech startup.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact

Search: