Re:Show HN: Dependently typed language for proofs that you c...
by erichocean on Saturday October 02, 2021 @12:19PM
(#28729792)
> 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.
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.