For sure not, otherwise those languages will contradict Gödel’s incompleteness: they must have a way to decide the emptiness or not of any of their types.
1 Like
(EDIT: clicked the wrong Reply button, this is not in response to @kantian specifically.)
Notice my posts were only on trying to convey what, I think, Lamport alludes to. I’m not in any way saying that you couldn’t have a better (w.r.t. some criterion to be defined) logical system than that of TLA+. I obviously don’t say that Coq, etc. don’t “abstract above the code level”.
Lamport is pretty consistent in that (1) he wants to model and prove properties of concurrent and distributed algorithms in a “straightforward” way (and for this, having the possibility to model fairness, for instance, is very important) and (2) he wants to rely on good-old set theory to do so (he doesn’t need to formalise algebraic structures or cryptography). He doesn’t want to show that you can encode LTL + set theory in a proof assistant and then possibly prove some properties of a couple of algorithms; he wants to use them out of the box and prove properties of dozens of algorithms.
Also, I was not talking about model-checking. TLA+ was, more then 30 years ago, created to write down proofs of algorithms and Lamport was reluctant on using m-c. I’m not a specialist of the proof system of TLA+, but AFAIK it can mainly check proofs but doesn’t really help you writing them the way a proof assistant does, so we are very far from the level of sophistication of Coq, Isabelle and the like. But the proofs Lamport can write thanks to TLA proof rules are rather straightforward, if cumbersome, and that suits him (not me, to be honest 
).
Model-checking is certainly limited. But the work to find and prove a good invariant is hard and m-c helps tremendously in finding corner-cases and assist in devising helper invariants. Liveness properties also benefit from this. My limited experience is that it’s far easier to begin with an m-c and switch to a proof once you don’t find counter-examples anymore. As the joke goes: if it’s true for 3, it’s true for n; for distributed systems, it can often be the case indeed.
Notice however that m-c can “prove” things even on unbounded systems in certain, limited cases, thanks to some forms so-called “small model properties” for certain fragments of first-order LTL (to be honest, this is limited in scope due to the restriction on the said fragments, but with some over-approximation, you can still do nice things as my PhD student did).
1 Like
No problem. But, I don’t know what to answer. I never had the intention to criticize TLA+ or to to say that we can do better (for sure it’s always possible, as most of what humanity has already created). My only point was to explore the meaning of “abstracting above the code level”. In dependently typed language we can do so: proofs are lambda terms evaluated at compile time and then disappear at runtime, i.e. at the “code level” (as in OCaml but in a more powerful way).
Then Lamport and TLA+ may be of great use, whit their advantages and drawbacks. I don’t really know, this system is not intended to me.
Maybe, the “a run for its money” of @xavierleroy maid you believe the contrary, but I’m not sure it was its intention (maybe it was, but I can’t answer for him).
2 Likes
As I said, it what not specifically in response to you so you don’ t have to answer 
I get it and I actually agree. My own point was rather to point that IMO, in this video, Lamport doesn’t speak so much of being above the code by proving things about programs (whether in a dependently-typed language or other forms of proof assistants) but rather because TLA+ features, at the language level, useful constructs to describe “systems”.
Then indeed, I think there is an academic separation, in practice (this is notably very clear in conferences), between the field of proof assistants (in particular type-theory-based ones) and that of “formal specification” (let’s call it this way). That’s a pity considering people in both these fields supposedly want to provide means to achieve safer software.
1 Like
I wasn’t aware of this. I’m not a researcher, I don’t have any PhD, so even not PhD student. But I agree, It’s a pity that people that have the same project can’t agree on the method (naturally, I will go to the logical one, but I’m partial, logic is the foundation of all my knowledge). But, maybe, each camp has its good reasons.
2 Likes
Maybe my “run for the money” comment was ambiguous. I was not criticizing TLA+'s logic, which as far as I know is a respectable set theory, although I regret that it is untyped. I was emphasizing that the constructive, typed logics you get in Agda, Coq or Lean are amazingly powerful and expressive, even though (or because?) they are just the Curry-Howard image of typed functional programming languages. In particular, inductive predicates, which are essentially GADTs, are an incredibly powerful tool for specification and proof.
1 Like
I found this elaboration and clarification very illuminating. Thanks!
This makes a lot of sense, and is quite cool. I think this is the kind of thing I have in mind for ways of getting mutually beneficial exchange from the model checking and theorem proving approaches. I think I finally, properly understand your point about the modeling and proving using TLA+, and how that is separate from the use of model checking in this context. Thank you for explaining.
To clarify regarding
I didn’t mean to suggest you were saying this. That question on my part was meant to go back to the general question of this post, but I didn’t signal that very well. I think your remark here helps to clarify (for me) what is going:
I guess part of the difficulty (for me) in fully appreciating (or accepting) this perspective as it pertains to programming languages must come from the fact that in the propositions-as-types approach, we also have language-level constructs to describe systems, and reasoning about the programs in the language is the way we reason about the system so described. I do think I understand and accept your point, tho, that the special-purpose design of TLA+ (and it’s ability to ignore any concerns of maintaining isomorphism (not to mention identification) with programs) has enabled it to be very expressive and concise, and obviously used to good effect.
Again, very interesting for me to read your reflections here, @grayswandyr. Thank you
1 Like
In case it would be of interest to you or others, Apalache supports a typed subset of TLA+ and can typecheck TLA+ specs (sometimes requiring a bit of additional annotation).
In case you haven’t thought of this already, @2BitSalute, if you are interested in finding more thoughts on this question, you might also considering asking the TLA+ User Group. You might also find some interesting prior discussion there, like this remark from Lamport, where he gives a pretty clear characterization of “thinking above the code level”:
Thinking above the code level means
describing/specifying/modeling what you’re doing. You should always
do that. In some cases, you will want to write that
description/specification/model in a formal language. The main reason
for doing that is so you can use tools to check it. Occasionally,
what you’re doing is so subtle and hard to understand that it’s worth
using a formal language even if you’re not using tools. But even if
you don’t use a formal language, it’s important to write down that
description/spec/model–because that’s the only way to be sure you
understand it. Comments in the code are often a good place to write
it.
I think this helps me understand my own thinking on this better too. And, IMO, it validates the view that languages like OCaml, and even more so programming languages like Coq, Lean, F* etc., do indeed include tools for formalizing thinking above the code level, in the sense Lamport means.
The discussion here also reminds me of this lovely passage from “The Art of Prolog”:
We believe that programming can be, and should be, an intellectually rewarding activity; that a good programming language is a powerful conceptual tool — a tool for organizing, expressing, experimenting with, and even communicating one’s thoughts … we think that programming can be, and should be, part of the problem solving process itself; that thoughts should be organized as programs, so that consequences of a complex set of assumptions can be investigated by “running” the assumptions; that a conceptual solution to a problem should be developed hand-in-hand with a working program that demonstrates it and exposes its different aspects.
As I read it, this encourages us to consider the value of programs in helping us achieve an understanding of what we are doing! (This also points back to some of the virtue of the propositions-as-types approach, IMO :D).
(Sorry for the multiple posts! I forgot to include all my replies in the previous one.)
2 Likes
To this question, I would answer “because” but I’m clearly biased on this subject. Curry-Howard, from a kantian point of view, is just a particular case of a more general principle already stated by Kant in 1781, and it’s only the way human mind is formally structured. See this chapter of Critique of pure reason, especially the correspondence between the tables in section II and III.
1 Like
Coming myself from a type theory-related PhD, and being a fervent OCaml-er, it took me a long time, even after reading his famous dialogue with Paulson, to get a grasp of why Lamport insists on TLA (the logic underlying TLA+) to be untyped. My supposition, but I may very well be wrong, is the following: when Lamport created TLA+, he thought of types as invariants that are stated to hold in every state, which can be problematic, in particular when reasoning on the enabledness of actions (which is required for fairness assumptions). My feeling is that type inference rather than type verification could reconcile TLA+ (or a successor) with types (I don’t know the inner working of Appalache and that may be what they do actually).
2 Likes
To say a little more, TLA+ allows to specify with one-liners that no process is infinitely faster than the others, or that no process will forever overwrite your mailbox effectively preventing you to see a certain message, or that the communication has this or that property (duplication, loss, ordering…). There’s nothing absolutely specific to TLA+ and this can be implemented in proof assistants but not with the same level of user-friendliness until now, as far as I know (and I would not claim TLA+ is that user-friendly ).
1 Like