3 ms·

Is TLA+ similar to Alloy[1]? 1. http://alloy.mit.edu/alloy/ http://alloy.mit.edu/alloy/

colanderman 9y ago
In that they're both modeling languages, yes. Alloy is more geared toward algorithms, while TLA+ is more geared toward concurrent systems. This paper has a good comparison: https://arxiv.org/abs/1603.03599 https://arxiv.org/abs/1603.03599
- pron 9y ago
  TLA+ is not a model checker. It is a specification and proof language. However, it has verification tools that include a model checker (TLC) and a mechanical proof system (TLAPS), both support a large and useful subset of the language. There are also other TLA+ model checkers under development or already available with some effort. In many ways it is more similar to Coq and Isabelle than to Alloy. For one, it has proof of relative completeness: anything that can be proven about a system, can be proven in TLA+. But because a model-checker makes a huge difference in productivity (it is usually the difference between worth it and not worth it), it TLA+ is similar to Alloy in terms of the effort required. Also, while it is harder to learn than Alloy, it is much easier to learn than Coq or Isabelle; partly due to design and partly due to the fact you can use it without learning how to be effective at writing formal, mechanically-chcekable proofs. It takes about two weeks to learn TLA+ well enough to start getting real work done. OTOH, while TLA+ can in principle be used to prove general mathematical theorems, it was designed with a focus on discrete systems (i.e., software and hardware) and targeted at engineers, not mathematicians/logicians, so if you want to do general formal math, Isabelle or Coq would be a better choice.
  - colanderman 9y ago
    Yes I misspoke, but, for the purposes of the article, the GP's question, and the use to which most readers here will put TLA+, it's tied at the hip to TLC and is used primarily for model checking.
nickpsecurity 9y ago
Here's the comparison I found: https://groups.google.com/forum/m/#!topic/tlaplus/C7Rmka3iSGE https://groups.google.com/forum/m/#!topic/tlaplus/C7Rmka3iSG... Alloy is a nice tool. I've seen it in my field used to verify transaction handling in simple databases and part of a high-assurance VPN. Another person here said they check data structures with it.

In that they're both modeling languages, yes. Alloy is more geared toward algorithms, while TLA+ is more geared toward concurrent systems. This paper has a good comparison: https://arxiv.org/abs/1603.03599 https://arxiv.org/abs/1603.03599

pron 9y ago
TLA+ is not a model checker. It is a specification and proof language. However, it has verification tools that include a model checker (TLC) and a mechanical proof system (TLAPS), both support a large and useful subset of the language. There are also other TLA+ model checkers under development or already available with some effort. In many ways it is more similar to Coq and Isabelle than to Alloy. For one, it has proof of relative completeness: anything that can be proven about a system, can be proven in TLA+. But because a model-checker makes a huge difference in productivity (it is usually the difference between worth it and not worth it), it TLA+ is similar to Alloy in terms of the effort required. Also, while it is harder to learn than Alloy, it is much easier to learn than Coq or Isabelle; partly due to design and partly due to the fact you can use it without learning how to be effective at writing formal, mechanically-chcekable proofs. It takes about two weeks to learn TLA+ well enough to start getting real work done. OTOH, while TLA+ can in principle be used to prove general mathematical theorems, it was designed with a focus on discrete systems (i.e., software and hardware) and targeted at engineers, not mathematicians/logicians, so if you want to do general formal math, Isabelle or Coq would be a better choice.
- colanderman 9y ago
  Yes I misspoke, but, for the purposes of the article, the GP's question, and the use to which most readers here will put TLA+, it's tied at the hip to TLC and is used primarily for model checking.

nickpsecurity 9y ago

Here's the comparison I found: https://groups.google.com/forum/m/#!topic/tlaplus/C7Rmka3iSGE https://groups.google.com/forum/m/#!topic/tlaplus/C7Rmka3iSG... Alloy is a nice tool. I've seen it in my field used to verify transaction handling in simple databases and part of a high-assurance VPN. Another person here said they check data structures with it.