> ...Only if you're trying to represent temporal logic in some functional language
Well, since the user was specifically asking for a comparison of TLA+ with systems like Coq, Agda and Idris, I should think that the question "how would I represent the logic TLA uses, given a language like Coq/Agda/Idris i.e. a functional (dependently-typed) language?" is quite relevant! (Perhaps even more relevant than the issue of what happens to be better known among academics in the formal-methods community.)
> 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
This is of course true if the model checking is exhaustive. Given that TLA+ is most often tuned "for use in industry on large, real-world systems" however, most uses of model checking are probably not going to exhaustively check the relevant state space.
(Similar to the underlying reason why the vast majority of users in industry would probably focus on the model-checking component in TLA+, not the fact that it also happens to include a proof assistant.)
> ...Now, all formal methods -- whether Coq or TLA+ -- have severe scalability limitations. Very roughly, one could verify about 2000 lines of specification...
(This is of course a very real challenge, but type checkers are far more scalable than that, and there are reasons to expect that this may generalize to other "local", "shallow" properties like simple checking of pre- and post- conditions ("design by contract"), or the sort of resource-based and region-based checking that is now being used for systems like Rust. This is where end-to-end methods might have real potential.)
> This is of course true if the model checking is exhaustive.
If it isn't exhaustive, it isn't model checking (i.e. it doesn't check that your program/spec is a model of a formula that describes some correctness property).
> most uses of model checking are probably not going to exhaustively check the relevant state space.
Ah, so what happens there is that you check a finite instance derived from your specification. I.e., instead of checking a specification for n ∈ Nat, you check a derived specification where n ∈ 0..4. But it's a proof of the correctness for the specification that is actually checked. Obviously, a model checker can't prove something it can't check (same goes for deductive proofs).
> Perhaps even more relevant than the issue of what happens to be better known among academics in the formal-methods community.
Definitely temporal logic, then :) FP is rare in formal methods, but is well known in programming language research. There is a small intersection of the two fields (proof assistants, dependent types), but I doubt it even makes out 10% of formal methods research (most of which is around model checking and static analysis).
> but type checkers are far more scalable than that, and there are reasons to expect that this may generalize to other "local", "shallow" properties like simple checking of pre- and post- conditions ("design by contract"), or the sort of resource-based and region-based checking that is now being used for systems like Rust. This is where end-to-end methods might have real potential.
We know what kind of properties you can scale, and the method of checking them -- either by type checking or any other form of abstract interpretation -- is not relevant (none can do a better job than the others). Those are inductive (or, since if you like programming language theory, the compositional) properties. Unfortunately, most deep properties are not inductive; this means that proving them using scalable inductive techniques (type preservation is an inductive property as are the inferences in any deductive system) would always require a long proof, that exists somewhere in a huge search space.
So, type checkers, model checkers and static analysis are all scalable for the same properties, and not scalable also for the same ones.
Also, there are no end-to-end methods, as far as I know. There are just projects small enough, and people devoted enough to do incredibly tedious work.
Well, since the user was specifically asking for a comparison of TLA+ with systems like Coq, Agda and Idris, I should think that the question "how would I represent the logic TLA uses, given a language like Coq/Agda/Idris i.e. a functional (dependently-typed) language?" is quite relevant! (Perhaps even more relevant than the issue of what happens to be better known among academics in the formal-methods community.)
> 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
This is of course true if the model checking is exhaustive. Given that TLA+ is most often tuned "for use in industry on large, real-world systems" however, most uses of model checking are probably not going to exhaustively check the relevant state space.
(Similar to the underlying reason why the vast majority of users in industry would probably focus on the model-checking component in TLA+, not the fact that it also happens to include a proof assistant.)
> ...Now, all formal methods -- whether Coq or TLA+ -- have severe scalability limitations. Very roughly, one could verify about 2000 lines of specification...
(This is of course a very real challenge, but type checkers are far more scalable than that, and there are reasons to expect that this may generalize to other "local", "shallow" properties like simple checking of pre- and post- conditions ("design by contract"), or the sort of resource-based and region-based checking that is now being used for systems like Rust. This is where end-to-end methods might have real potential.)