Hacker News new | past | comments | ask | show | jobs | submit login

> A proposition is not a set in any conceivable setting.

What you called "predicate" in your other comment, is a proposition in a logic that expresses machines in a certain way (where the object of the predicate, i.e. the machine, is implicit). TLA is a (linear) temporal logic, and so, like all temporal logics (at least those concerning computer programs) its structure is an abstract state machine (which, BTW, can also describe LC, either by choosing an evaluation strategy, in which case the machine is deterministic, or not -- treating it as an abstract rewriting system -- in which case the machine is nondeterministic).

> It's external because it's not a part of Java or whatever other language you're using to write your actual program.

Now you completely lost me. You said "In TLA+, or any other external program logic, the program itself is just a syntactic object". In TLA+, the only notion of "the program itself" is the TLA+ expression. Whether your TLA+ expression is automatically generated from Java or C code (as some research teams have done) or coded manually, the other representation is not an object in TLA+ at all. It's like saying that if I implement quicksort in Java and you implement it in C, then your program is a syntactic object of mine. I'm not sure what it means. When you code quicksort in TLA+, TLA+ is not aware in any shape or form of any other existing or possible representations.

Unrelated to your statement about external logics, it is obviously true that TLA+ is not used as a programming language (I guess it could be, but it would be extremely inefficient[1]) but a specification language. TLA+ is used across many companies in the industry to specify systems that are very large (the program I alone verified in a few months is many times bigger than seL4 or CompCert), and therefore full end-to-end language-level (or extracted) verification does not apply to them anyway. TLA+ provides a different level of guarantees, but also aims at a different scale of programs (Lamport: "The development of TLA+ was motivated by the needs of engineers building large systems, for which complete formal development is out of the question."[2])

[1]: Synchronous programming languages (like Esterel, or the modern Céu) share some similarities with TLA, and indeed Esterel and its descendants are used in the industry to write and verify safety-critical real-time systems (esp. avionics and other embedded software). However, in Esterel (unlike TLA+) the LTL propositions are indeed distinct from the program, and are therefore external.

[2]: http://research.microsoft.com/en-us/um/people/lamport/pubs/c...




Again, perhaps I've complicated simple things unnecessarily:

> A proposition is not a set in any conceivable setting.

A proposition can be seen as a predicate over the logic's structures, and therefore a set of structures. TLA is a logic whose structures are abstract state machines (and therefore the machine is implicit). Any proposition in TLA is therefore a predicate over programs, or a set of them, and is, therefore, runnable.

But since I've added this comment, let me give a specific example. The TLA+ statement `A ≜ x = 3 ∧ (x' = x)` says that the value of variable x in the machine's initial state is 3, and it never changes. It can also be viewed as the set of all programs with this behavior. If we add the following statement, `VARIABLES x`, we tell TLA+ that variable x is the only variable we care about (of all infinite variables), and at this point the proposition is runnable, because all (infinitely many) machines would appear to behave in the same way with regards to variable x, so we may as well imagine that x is the only variable. "Running" within this logic, then, means visiting all states of all possible machines where the proposition holds true.

Now, let's define proposition B: `B ≜ x = 3 ∧ y ∈ {-1, 1} ∧ (x' = x ∧ y' ∈ {-1, 1})`. This is a proposition about the behavior of two variables, but also a description of a nondeterministic program (in which at any state, y can take the value 1 or -1), which we can run (once we tell TLA+ `VARIABLES x, y`).

Now we can also write `B ⇒ A` -- we say B implements A -- (which is true) and semantically means that B is a simulation of A (or a trace-subset; I'm not sure, but I think it's the same as far as we're concerned), but this is just a restatement of treating `⇒` as the familiar implication connective within the modal (temporal) logic. "Running" `B ⇒ A` is the same as running B, but visiting all states where `B ⇒ A` is true, which is everywhere. Similarly, we can define `C ≜ x = 3 ∧ y' ∈ {-1, 1} ∧ (x' = x ∧ y' = -y)` which is still nondeterministic but now has only two possible behaviors, and it is true that `C ⇒ B`. If `D ≜ x = 3 ∧ y' = 1 ∧ (x' = x ∧ y' = -y)`, then D is now fully deterministic, and D ⇒ C (and therefore D ⇒ B and D ⇒ A).




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: