4 ms·

What is the difference between formal methods as implemented by TLA+, proof assistants like Coq, and theorem proving languages like Agda (Idris?)?

by mjfl 8y ago

jlrubin 8y ago
coq allows you to extract a real program, whereas TLA+ just checks a spec for correctness (and you may have bugs implementing it)
- pron 8y ago
  See my other comment on the matter, but this presents a choice where there is none. No tool that extracts or verifies actual code (and people have actually done both with TLA+) can operate on programs larger than a few thousand lines. So it's not a choice between fully verifying a 200KLOC program or just its 2000-line high-level spec. It's between verifying/extracting a 2000 line program or a 2000 line spec that abstracts a 200KLOC program. In other words, for programs of a certain size, verifying a high-level spec is the only real option for "deep" verification.
- hwayne 8y ago
  I've seen research tools to extract "real programs" from TLA+. But on the whole not having synthesis as your default case has two major advantages: 1. You can choose the level of modeling, so you can quickly spec out the high level and find bugs in that before moving on to the low level (if you want) 2. It doesn't tie you to an implementation language. So you can use it even if you're implementing in COBOL, JavaScript, or Brainfuck. Of course extraction has its own benefits. Coq is a pretty cool tool :)
0815test 8y ago
TLA+ uses model checking over what can be understood as a custom modal logic-- the latter means that TLA is basically adding a bunch of modalities (which could also be understood as (co-)monads) that allow for the modeling of state ("temporal" logic), nondeterminism (which also shows up in the modeling of abstraction/refinement relations) and perhaps some other features, over the basic logic that you would find pre-defined in most theorem provers. The use of model checking means that TLA+ is basically a glorified fuzzer: it will attempt to find a refutation of the model you define (such a model, in turn is usually an abstraction of the system you actually care about; not something that gets verified "end-to-end" like in Agda or Coq) and any such refutation will be a genuine proof that the model fails in some way; but a failure to find one does not amount to a proof of correctness!
- pron 8y ago
  > a custom modal logic TLA, the logic at the heart of TLA+, is a linear temporal logic, which is, indeed, an example of a modal logic, but also the most ubiquitous and successful type of logic in program verification. I think that in computer science in general and formal methods in particular, temporal logic is more well known than all other modal logics combined (and probably more than even the name or concept of modal logic). > which could also be understood as (co-)monads This is only relevant if you're trying to represent temporal logic in some functional language, which TLA+ isn't. > The use of model checking TLA+ is a specification (and proof) language that's independent from how it's verified (or how the proof are checked). There is a model checker for TLA+, as well as a proof assistant. > a glorified fuzzer Model checkers and fuzzers are not at all alike. A fuzzer runs a program many times, while a model checker doesn't run it even once, but rather checks it. To see how different checking is from running, consider that a model checker like TLC (a model checker for TLA+) could completely check in a number of seconds an infinite (and even uncountable) number of executions, each with an infinite number of steps. > a failure to find one does not amount to a proof of correctness! A failure to find a counterexample most definitely amounts to a proof of correctness. It is not a deductive proof in the logic, but a proof nonetheless (one that employs the model theory of the logic as opposed to its proof theory). That's the meaning of the term "model checker": it automatically checks whether some program is a model for some formula (i.e. a structure that satisfies the formula). > not something that gets verified "end-to-end" like in Agda or Coq This is misleading. It is possible to do "end-to-end" in TLA+, pretty much as it is is in Coq, which is to say that it's possible only on very small programs, usually in research settings. For example, see here[1]. But the main difference between TLA+ and Coq/Agda is that it's not a research tool but a tool intended for use in industry on large, real-world systems. Now, all formal methods -- whether Coq or TLA+ -- have severe scalability limitations. Very roughly, one could verify about 2000 lines of specification -- that specification can be actual code (i.e. a ~2000 line program) or a high-level spec that abstracts 200K or even 2M lines of code. Because TLA+ is intended for use in industry, it is designed to be used on high-level specs more than code, because most programs that require verification are not small enough. But if you have a 200K-2M LOC program, it's not as if end-to-end verification is a choice. Remember that the biggest programs ever to be fully verified end-to-end were about 1/5 the size of jQuery, and took world experts years of effort -- not a feasible option for most software. [1]: https://www.researchgate.net/publication/281886818_An_Approach_for_Verifying_Concurrent_C_Programs https://www.researchgate.net/publication/281886818_An_Approa...
pron 8y ago
They are many similarities and many differences, but the differences mostly stem from their goals being very different. Coq, Agda and Idris are mostly used for research. TLA+ is designed for heavy-duty, everyday use in industry by software and hardware developers working on large, complex real-world systems.
- deleted 8y ago
  [deleted]
- hwj 8y ago
  AFAIK Coq is used by CompCert[0], which is used for safety-critical software in the industry[1]. [0] http://compcert.inria.fr/ http://compcert.inria.fr/ [1] https://www.absint.com/index.htm https://www.absint.com/index.htm
  - pron 8y ago
    CompCert is written in Coq, and was developed as a research project at academic institutions [1]. It's a very small program (about 1/5 the size of jQuery) that has taken world-experts years to develop. [1]: https://en.wikipedia.org/wiki/CompCert https://en.wikipedia.org/wiki/CompCert
strangecasts 8y ago
Very broadly: model checkers (which most TLA+ users use) verify systems by induction, by enumerating possible states a system can take on, and showing that the none of the states violate the system requirements. In comparison, proof assistants take a deductive approach, requiring you to show - step by step - how the requirements are satisfied by the definition of the system. Dependently typed languages move some of that burden to the type system.
- duality 8y ago
  TLC is the model checker that operates on TLA+ specs. TLAPS is a proof system. So, TLA+ has both.
  - strangecasts 8y ago
    Yep :) Hence "most" - you can write deductive proofs with TLAPS, but most of the documentation and the community is devoted to model-checking.

What is the difference between formal methods as implemented by TLA+, proof assistants like Coq, and theorem proving languages like Agda (Idris?)?

by mjfl 8y ago

What is the difference between formal methods as implemented by TLA+, proof assistants like Coq, and theorem proving languages like Agda (Idris?)?

jlrubin 8y ago

coq allows you to extract a real program, whereas TLA+ just checks a spec for correctness (and you may have bugs implementing it)

pron 8y ago
See my other comment on the matter, but this presents a choice where there is none. No tool that extracts or verifies actual code (and people have actually done both with TLA+) can operate on programs larger than a few thousand lines. So it's not a choice between fully verifying a 200KLOC program or just its 2000-line high-level spec. It's between verifying/extracting a 2000 line program or a 2000 line spec that abstracts a 200KLOC program. In other words, for programs of a certain size, verifying a high-level spec is the only real option for "deep" verification.
hwayne 8y ago
I've seen research tools to extract "real programs" from TLA+. But on the whole not having synthesis as your default case has two major advantages: 1. You can choose the level of modeling, so you can quickly spec out the high level and find bugs in that before moving on to the low level (if you want) 2. It doesn't tie you to an implementation language. So you can use it even if you're implementing in COBOL, JavaScript, or Brainfuck. Of course extraction has its own benefits. Coq is a pretty cool tool :)

0815test 8y ago

TLA+ uses model checking over what can be understood as a custom modal logic-- the latter means that TLA is basically adding a bunch of modalities (which could also be understood as (co-)monads) that allow for the modeling of state ("temporal" logic), nondeterminism (which also shows up in the modeling of abstraction/refinement relations) and perhaps some other features, over the basic logic that you would find pre-defined in most theorem provers. The use of model checking means that TLA+ is basically a glorified fuzzer: it will attempt to find a refutation of the model you define (such a model, in turn is usually an abstraction of the system you actually care about; not something that gets verified "end-to-end" like in Agda or Coq) and any such refutation will be a genuine proof that the model fails in some way; but a failure to find one does not amount to a proof of correctness!

pron 8y ago
> a custom modal logic TLA, the logic at the heart of TLA+, is a linear temporal logic, which is, indeed, an example of a modal logic, but also the most ubiquitous and successful type of logic in program verification. I think that in computer science in general and formal methods in particular, temporal logic is more well known than all other modal logics combined (and probably more than even the name or concept of modal logic). > which could also be understood as (co-)monads This is only relevant if you're trying to represent temporal logic in some functional language, which TLA+ isn't. > The use of model checking TLA+ is a specification (and proof) language that's independent from how it's verified (or how the proof are checked). There is a model checker for TLA+, as well as a proof assistant. > a glorified fuzzer Model checkers and fuzzers are not at all alike. A fuzzer runs a program many times, while a model checker doesn't run it even once, but rather checks it. To see how different checking is from running, consider that a model checker like TLC (a model checker for TLA+) could completely check in a number of seconds an infinite (and even uncountable) number of executions, each with an infinite number of steps. > a failure to find one does not amount to a proof of correctness! A failure to find a counterexample most definitely amounts to a proof of correctness. It is not a deductive proof in the logic, but a proof nonetheless (one that employs the model theory of the logic as opposed to its proof theory). That's the meaning of the term "model checker": it automatically checks whether some program is a model for some formula (i.e. a structure that satisfies the formula). > not something that gets verified "end-to-end" like in Agda or Coq This is misleading. It is possible to do "end-to-end" in TLA+, pretty much as it is is in Coq, which is to say that it's possible only on very small programs, usually in research settings. For example, see here[1]. But the main difference between TLA+ and Coq/Agda is that it's not a research tool but a tool intended for use in industry on large, real-world systems. Now, all formal methods -- whether Coq or TLA+ -- have severe scalability limitations. Very roughly, one could verify about 2000 lines of specification -- that specification can be actual code (i.e. a ~2000 line program) or a high-level spec that abstracts 200K or even 2M lines of code. Because TLA+ is intended for use in industry, it is designed to be used on high-level specs more than code, because most programs that require verification are not small enough. But if you have a 200K-2M LOC program, it's not as if end-to-end verification is a choice. Remember that the biggest programs ever to be fully verified end-to-end were about 1/5 the size of jQuery, and took world experts years of effort -- not a feasible option for most software. [1]: https://www.researchgate.net/publication/281886818_An_Approach_for_Verifying_Concurrent_C_Programs https://www.researchgate.net/publication/281886818_An_Approa...

pron 8y ago

They are many similarities and many differences, but the differences mostly stem from their goals being very different. Coq, Agda and Idris are mostly used for research. TLA+ is designed for heavy-duty, everyday use in industry by software and hardware developers working on large, complex real-world systems.

deleted 8y ago
[deleted]
hwj 8y ago
AFAIK Coq is used by CompCert[0], which is used for safety-critical software in the industry[1]. [0] http://compcert.inria.fr/ http://compcert.inria.fr/ [1] https://www.absint.com/index.htm https://www.absint.com/index.htm
- pron 8y ago
  CompCert is written in Coq, and was developed as a research project at academic institutions [1]. It's a very small program (about 1/5 the size of jQuery) that has taken world-experts years to develop. [1]: https://en.wikipedia.org/wiki/CompCert https://en.wikipedia.org/wiki/CompCert

strangecasts 8y ago

Very broadly: model checkers (which most TLA+ users use) verify systems by induction, by enumerating possible states a system can take on, and showing that the none of the states violate the system requirements. In comparison, proof assistants take a deductive approach, requiring you to show - step by step - how the requirements are satisfied by the definition of the system. Dependently typed languages move some of that burden to the type system.

duality 8y ago
TLC is the model checker that operates on TLA+ specs. TLAPS is a proof system. So, TLA+ has both.
- strangecasts 8y ago
  Yep :) Hence "most" - you can write deductive proofs with TLAPS, but most of the documentation and the community is devoted to model-checking.