3 ms·

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 go

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 10y 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 10y 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.

3 ms·

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 go

by colanderman 10y ago

pron 10y 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 10y 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.