3 ms·

> That boolean expression is not a proposition about the program -- that is correct -- but the distinction may be artificial. A Java `boolean` expression isn't

> That boolean expression is not a proposition about the program -- that is correct -- but the distinction may be artificial. A Java `boolean` expression isn't a proposition about anything. A proposition might be, say, the assertion that the expression always evaluates to `true`, but this is inexpressible in Java itself. > You may be used to languages where there's a clear distinction between program properties and program code, but if you think about it, that distinction is artificial. The distinction I made wasn't between program properties and program code, and in certain programming languages (say, Agda), propositions themselves can be normal code. But Java doesn't have propositions at all, so if you need to express propositions, you'll have to use an external logic. > For me, a proposition about code is a set of TMs with a property (in particular, safety properties are a closed set of TMs, and liveness properties are dense etc. etc.). This is just wrong, and it has nothing to do with types. Even a set theorist would disagree with you. A proposition is not a set in any conceivable setting. > Its truth value is whether your program is in this set or not. To be more precise, a proposition to me is a sentence in any logic denoting that set. The denotation of a proposition is always a truth value. > Does the proposition "the program returns a list containing exactly the same elements in its input, each appearing the same number of times, only in sorted order" has a runtime computational relevance or not? It does not. It's simply a fact about your program. Your program can't branch on it. > TLA+ is not an external program logic, but a complete logic It's external because it's not a part of Java or whatever other language you're using to write your actual program. And nothing prevents an external logic from being “complete” or whatever other desirable property you want - in fact, the very reason for using external program logics is to avoid the limitations of the language your program is written in!

pron 10y ago
> 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/commentary-web.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/c...
- pron 10y ago
  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).

pron 10y ago

> 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/commentary-web.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/c...

pron 10y ago
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).