3 ms·
The vast majority of people using languages like Coq, Isabelle, or Lean, are researchers, and those tools are designed for research (such as defining and explor
by pron 4y ago
The vast majority of people using languages like Coq, Isabelle, or Lean, are researchers, and those tools are designed for research (such as defining and exploring new logical systems). TLA+, on the other hand, is designed for practitioners, i.e. people who build systems for a living. That is why more papers are being written about Coq and Isabelle, but more bugs in more real-world systems are being found with TLA+. So it depends on what your job is.
- avgcorrection 4y ago
- anonymousDan 4y agoYes the people I am referring to are in the business of designing and proving new distributed algorithms and proving/disproving the correctness of existing existing well-known algorithms for which only handwavy proofs have been provided. In particular it goes beyond just model checking.
- pron 4y agoRight. TLA+ has a proof assistant, just as Coq and Isabelle do, and it has been used to good effect. But because there is also a model-checker capable of checking (a subset of) TLA+ (actually, two model checkers now), practitioners greatly prefer using that over a proof assistant. The reason is that if your goal isn't to publish a paper but to deploy a system, what you're optimising for is bugs found per hour of effort, and a model-checker has a higher ROI in that regard than deductive proofs.