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

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.






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

Search: