[zozbot234]

> tl;dr TLA+ is a lot more practical if you care about bug-free software

TLA+ is not generally used for end-to-end checking of actual program code, unlike Coq. Usually you build a simplified "toy" model in TLA+ of some architecture of interest, then use model checking to try and refute some claimed properties of that model. If the model checker finds a refutation of some property, then yes, that's a verified bug in your toy model. If it fails to find one, that's not a proof of correctness other than in very special cases where a property can be checked finitely.

So yes, model checking is helpful in some cases, but it's not a generally useful tool. And there are ways to do the same things in general proof assistants, e.g. by interfacing them with external SMT tools. The TLA language in itself is also unproblematic, it simply adds modalities for time, state and non-determinism to ordinary logic, and there are well-known ways to convert ("embed") those features to a form that a proof assistant can work with.

[erichocean]

> TLA+ is not generally used for end-to-end checking of actual program code, unlike Coq.

To my knowledge, TLA+ is never used for checking program code. At least, I've never heard of anyone doing it.

> model checking is helpful in some cases, but it's not a generally useful tool

I strongly disagree. Spending time trying to "prove" in Coq an incorrect, flawed specification is an insane waste of time. A model checker can show you the problems in (literally) seconds.

Consider Raft, for instance, which was formally verified in Coq. You know what they did first? Write a TLA+ model, and then model check that until they got the design right. Trying to start in Coq (with an incorrect design) would not have been smart.

Model checkers are extremely useful tools.

----

Going further, the TLA+ spec of Raft is less that 500 lines.

The Coq proof of TLA+ is ~50,000 lines. It resulted in a verified implementation that to the best of my knowledge, no one uses in production.

It's a nice achievement, but in terms of usefulness? TLA+ has Coq beat by a country mile.

[zozbot234]

> Spending time trying to "prove" in Coq an incorrect, flawed specification is an insane waste of time. A model checker can show you the problems in (literally) seconds.

Sure, if there's anything a TLA+ model checker is good at it's searching for counterexamples. But in pretty much any case where such a search is computationally viable, it's also easy to set it up in a proof assistant. By and large, model checkers use the exact same toolset under the hood as the "sledgehammer" automated proof search in a proof assistant, such as SAT and SMT satisfiability solvers.

> It resulted in a verified implementation, that to the best of my knowledge, no one uses is production.

No one uses a TLA+ model directly in production either, because that's not what TLA+ is. The question only makes sense for a tool like Coq where one can work end-to-end with an actual implementation.

[erichocean]

> No one uses a TLA+ model directly in production either

This is false. Many, many companies use software derived from TLA+ models "directly in production." Amazon and Microsoft (Azure) are the two biggest examples. Neither relegate TLA+ usage to "R&D" on experimental system. Both are using it to develop and harden actual production systems used by millions (billions?) of people daily, and the TLA+ toolset is used daily by normal production engineers, not academics (as is true of Coq).

Coq is great, I like it a lot. As of 2021, it's not very practical for the kinds of problems normal software engineers encounter whereas TLA+ is.