3 ms·

> but a proposition can: it is a set Set theories are normally built on top of the apparatus of logic, so a proposition can't be a set. > (of programs, or Tur

> but a proposition can: it is a set Set theories are normally built on top of the apparatus of logic, so a proposition can't be a set. > (of programs, or Turing machines if you like; people in the verification community may say it's a set of states in a Kripke structure) Ah, I see. You aren't talking about general propositions. You're talking about assertions about program states that can be checked dynamically, but want to verify statically. You can't represent an arbitrary proposition as a data structure, but it's of course a-whole-nother matter if you can decide the proposition's truth value by evaluating a Java expression of type `boolean`. The `boolean` expression itself is still not a proposition, though. > but you can't deny that the two expressions of proposition, i.e., the dynamic `x < 10` and `T`, are distinct and "live" in two separate worlds. Most programming languages don't have propositions at all, for a very good reason: a proposition is the type of a programmer-supplied proof that has no runtime computational relevance, and how to integrate proofs into programming is still a research question whose answer language designers can't wait for. In Java, “the dynamic `x < 10`” is just a `boolean` expression - not a proposition! > E.g., in TLA+, an untyped logic (TLA+ZFC), the program and the propositions are the very same objects and not at all just a "data-level abstract syntax representation of propositions". In TLA+, or any other external program logic, the program itself is just a syntactic object. And by extension so is any `boolean` expression the program might contain. OTOH, if Java had propositions, you could carry out your reasoning internally, side-stepping the need to encode propositions as abstract syntax for a metalanguage to see.

pron 10y ago
> Set theories are normally built on top of the apparatus of logic, so a proposition can't be a set. You don't need a set theory. P is a "naive" set. It's well defined no matter what, because TMs are a recursive set, and P is just a RE subset. You're not in danger of running into any sharp edges. > The `boolean` expression itself is still not a proposition, though. I'm not sure what you mean by that, but I think we're talking past each other. That boolean expression is not a proposition about the program -- that is correct -- but the distinction may be artificial. 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. For example, the expression `IF x > 0 THEN x ELSE -x` can be understood to be a program description taking the absolute value, but it can also be a proposition, or a description of the set of programs returning the absolute value of their input. Your language may use the same expression in both cases, yet still make a distinction about its meaning based on where it is used. Another language (like TLA+) has no such distinction. > a proposition is the type of a programmer-supplied proof that has no runtime computational relevance That's your definition. 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.). 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. I think my definition is both more encompassing and more precise than yours. It is more encompassing because every proposition by your definition is a proposition by my definition; it is more precise because the converse may not be true (although, again, I'm not certain about what your definition really means, its ties to a specific language, or whether or not it applies only to denotational semantics of programs). > has no runtime computational relevance I'm not sure what you mean by that. 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? > In TLA+, or any other external program logic, the program itself is just a syntactic object. TLA+ is not an external program logic, but a complete logic -- i.e. a TLA+ expression can describe any unique and arbitrary TM, or a set of them -- and there is no difference between a program and a proposition about a program in TLA+. The program is certainly not a syntactic element in TLA+ (certainly no more than any proposition is a syntactic element). Conceptually, in TLA+ you can describe the set of all programs that perform quicksort (it can be more than one; TLA+ allows nondeterminism) and then ask whether quicksort implies sorting, or, in other words, whether the set of quicksort programs is a subset of all programs that sort their input. Both the program and the proposition are logical expressions (describing a set of TMs, if you will), and you may then try to prove that one implies the other (or any logical combination of the two): In a quest for minimality and orthogonality of concepts, TLA+ does not formally distinguish between specifications and properties: both are written as logical formulas, and concepts such as refinement, composition of systems or hiding of internal state are expressed using logical connectives of implication, conjunction, and quantification. Despite its expressiveness, TLA+ is supported by tools such as model checkers and theorem provers to aid a designer carry out formal developments.[1] [1]: http://www.loria.fr/~merz/papers/tla+logic2008.pdf http://www.loria.fr/~merz/papers/tla+logic2008.pdf
- pron 10y ago
  P.S. If you think about it, the conjunction of all true propositions about your program is the program (modulo the equality semantics of your logic). This is true whether or not your program is deterministic, or, in the case of LC, is a collection of state machines, depending on the evaluation strategy). Conceptually, then, there is no difference between a program and the true propositions about it. Some languages make a syntactic distinction between the two (Haskell), some languages use similar syntax but different semantics (Idris), and some make no syntactic or semantic distinction (TLA+): your program is a logical sentence (a conjunction of axioms, if you will), from which all true propositions about it can be derived (and, obviously, only those). A program is the complete axiomatization of all true propositions about it[1]. [1]: This may get more tricky if intuitionistic logic is used, where the program is actually the proof object of all true propositions, but I think that even in intuitionistic logic, the distinction may be artificial: a proof may be no more than a hidden proposition.
  - catnaroek 10y ago
    There's so much that's wrong with this comment. You're either ignorant of formal logic, or deliberately trolling. If the former: being ignorant isn't a crime, but pretending you know what you don't know is uncivilized. If the latter: of course trolling is uncivilized. Let's keep things civilized, okay? > If you think about it, the conjunction of all true propositions about your program is the program (modulo the equality semantics of your logic). This doesn't even make sense. A program can be run. What does it mean to “run a proposition”? Even if I charitably interpret that as “decide its truth value”, well, not all propositions are decidable! > your program is a logical sentence (a conjunction of axioms, if you will), What you can treat as a bunch of axioms is the semantics of your programming language of choice. But a program isn't the same thing as the language it's written in. > the distinction may be artificial: a proof may be no more than a hidden proposition. This isn't true in either classical or intuitionistic logic. A proposition has a truth value - a proof does not.
    - pron 10y ago
      > Let's keep things civilized, okay? Formal verification of large, very complex real-world systems is what I do all day every day. If you don't understand what it is that I'm saying (and that's my fault -- I'm probably not clear enough) you can just ask. I'm a practitioner, not a theoretician, so I may make mistakes, but I think that in this particular case you are too attached to the typed LC to consider other reasoning systems (which, BTW, happen to be far more prevalent in the verification community). > This doesn't even make sense. A program can be run. What does it mean to “run a proposition”? Let's step back and consider the theory and then get to the specifics. Consider the set of all TMs (perhaps TMs isn't the best name because it may imply a specific programming model, but that is not my intent; I'm using the term here interchangeably with an abstract state machine, or a program). Each and every one of them is "runnable", right? Each and every subset of that set also consists of TMs, which are also runnable, right? A proposition about a TM constitutes such a subset. Under certain conditions, you can incorporate all DTMs in the set corresponding to the proposition into a single NDTM, which can also be run. Hence, there is a direct correspondence between propositions about programs (e.g., the program returns its input sorted) and NDTMs. Hence, you can most certainly run a proposition about programs (though perhaps not all propositions). The temporal logic of actions (TLA) is a complete logic in the sense that for every NDTM (or a DTM as a special case) there exists a (non-unique) TLA expression, consisting of the simple logical connectives, the priming operator (an action) and possibly LTL operators (describing say, fairness, properties) that describes that particular TM. But, of course, a TLA expression can be less precise, and describe a whole set of TMs -- a proposition. Therefore in TLA, propositions and programs are the same object. Here's Lamport in the opening paragraph introducing TLA in the 1993 paper[1]: Correctness of [an] algorithm means that the program satisfies a desired property. We propose a simpler approach in which both the algorithm and the property are specified by formulas in a single logic. Correctness of the algorithm means that the formula specifying the algorithm implies the formula specifying the property, where implies is ordinary logical implication. FYI, that paper has 2458 citations and is far from obscure. This theory is much better known in the software verification community than type theory (certainly when you consider it within the greater framework of temporal logics, of which TLA is one), and has had a greater impact -- both academic and real-world -- on formal methods, at least so far. Specifying programs as propositions in temporal logics was a modern theoretical turning point in CS, and has yielded two or three Turing awards (Pnueli in '96, Clarke et al. in '07, and Lamport -- at least partly for this -- in '13). > Even if I charitably interpret that as “decide its truth value”, well, not all propositions are decidable! This is where things are a bit tricky. For a complete treatment see the preliminaries section in this '88 paper by Abadi and Lamport[2]. > A proposition has a truth value - a proof does not. Of course, but there's room for interpretation here (like I said, I'm not a type expert so I'm not 100% sure about it): `<x = 3, y = 5>` can be viewed as a proof object of the proposition `∃x,y ∈ 1..10 . x < y`, but it can also be viewed as the more precise proposition, `x = 3 ∧ y = 5`. Existential propositions (or types) can therefore be viewed as a set of multiple programs, while the proof object is a particular program, that could have been specified with a more precise proposition. That is what I meant when I said "hidden proposition". If you step back from typed LC and consider the original proof objects, those objects are just a series (a tree, actually) of logical deductions. Each of those deductions is a proposition. A proof is, therefore, a series of true propositions, each derived from the previous one using one of the deduction rules. You can certainly say, then, that a proof is a collection of hidden (true) propositions. [1]: http://research.microsoft.com/pubs/64074/lamport-actions.pdf http://research.microsoft.com/pubs/64074/lamport-actions.pdf [2]: http://research.microsoft.com/pubs/64046/abadi-existence.pdf http://research.microsoft.com/pubs/64046/abadi-existence.pdf

pron 10y ago

> Set theories are normally built on top of the apparatus of logic, so a proposition can't be a set. You don't need a set theory. P is a "naive" set. It's well defined no matter what, because TMs are a recursive set, and P is just a RE subset. You're not in danger of running into any sharp edges. > The `boolean` expression itself is still not a proposition, though. I'm not sure what you mean by that, but I think we're talking past each other. That boolean expression is not a proposition about the program -- that is correct -- but the distinction may be artificial. 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. For example, the expression `IF x > 0 THEN x ELSE -x` can be understood to be a program description taking the absolute value, but it can also be a proposition, or a description of the set of programs returning the absolute value of their input. Your language may use the same expression in both cases, yet still make a distinction about its meaning based on where it is used. Another language (like TLA+) has no such distinction. > a proposition is the type of a programmer-supplied proof that has no runtime computational relevance That's your definition. 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.). 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. I think my definition is both more encompassing and more precise than yours. It is more encompassing because every proposition by your definition is a proposition by my definition; it is more precise because the converse may not be true (although, again, I'm not certain about what your definition really means, its ties to a specific language, or whether or not it applies only to denotational semantics of programs). > has no runtime computational relevance I'm not sure what you mean by that. 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? > In TLA+, or any other external program logic, the program itself is just a syntactic object. TLA+ is not an external program logic, but a complete logic -- i.e. a TLA+ expression can describe any unique and arbitrary TM, or a set of them -- and there is no difference between a program and a proposition about a program in TLA+. The program is certainly not a syntactic element in TLA+ (certainly no more than any proposition is a syntactic element). Conceptually, in TLA+ you can describe the set of all programs that perform quicksort (it can be more than one; TLA+ allows nondeterminism) and then ask whether quicksort implies sorting, or, in other words, whether the set of quicksort programs is a subset of all programs that sort their input. Both the program and the proposition are logical expressions (describing a set of TMs, if you will), and you may then try to prove that one implies the other (or any logical combination of the two): In a quest for minimality and orthogonality of concepts, TLA+ does not formally distinguish between specifications and properties: both are written as logical formulas, and concepts such as refinement, composition of systems or hiding of internal state are expressed using logical connectives of implication, conjunction, and quantification. Despite its expressiveness, TLA+ is supported by tools such as model checkers and theorem provers to aid a designer carry out formal developments.[1] [1]: http://www.loria.fr/~merz/papers/tla+logic2008.pdf http://www.loria.fr/~merz/papers/tla+logic2008.pdf

pron 10y ago
P.S. If you think about it, the conjunction of all true propositions about your program is the program (modulo the equality semantics of your logic). This is true whether or not your program is deterministic, or, in the case of LC, is a collection of state machines, depending on the evaluation strategy). Conceptually, then, there is no difference between a program and the true propositions about it. Some languages make a syntactic distinction between the two (Haskell), some languages use similar syntax but different semantics (Idris), and some make no syntactic or semantic distinction (TLA+): your program is a logical sentence (a conjunction of axioms, if you will), from which all true propositions about it can be derived (and, obviously, only those). A program is the complete axiomatization of all true propositions about it[1]. [1]: This may get more tricky if intuitionistic logic is used, where the program is actually the proof object of all true propositions, but I think that even in intuitionistic logic, the distinction may be artificial: a proof may be no more than a hidden proposition.
- catnaroek 10y ago
  There's so much that's wrong with this comment. You're either ignorant of formal logic, or deliberately trolling. If the former: being ignorant isn't a crime, but pretending you know what you don't know is uncivilized. If the latter: of course trolling is uncivilized. Let's keep things civilized, okay? > If you think about it, the conjunction of all true propositions about your program is the program (modulo the equality semantics of your logic). This doesn't even make sense. A program can be run. What does it mean to “run a proposition”? Even if I charitably interpret that as “decide its truth value”, well, not all propositions are decidable! > your program is a logical sentence (a conjunction of axioms, if you will), What you can treat as a bunch of axioms is the semantics of your programming language of choice. But a program isn't the same thing as the language it's written in. > the distinction may be artificial: a proof may be no more than a hidden proposition. This isn't true in either classical or intuitionistic logic. A proposition has a truth value - a proof does not.
  - pron 10y ago
    > Let's keep things civilized, okay? Formal verification of large, very complex real-world systems is what I do all day every day. If you don't understand what it is that I'm saying (and that's my fault -- I'm probably not clear enough) you can just ask. I'm a practitioner, not a theoretician, so I may make mistakes, but I think that in this particular case you are too attached to the typed LC to consider other reasoning systems (which, BTW, happen to be far more prevalent in the verification community). > This doesn't even make sense. A program can be run. What does it mean to “run a proposition”? Let's step back and consider the theory and then get to the specifics. Consider the set of all TMs (perhaps TMs isn't the best name because it may imply a specific programming model, but that is not my intent; I'm using the term here interchangeably with an abstract state machine, or a program). Each and every one of them is "runnable", right? Each and every subset of that set also consists of TMs, which are also runnable, right? A proposition about a TM constitutes such a subset. Under certain conditions, you can incorporate all DTMs in the set corresponding to the proposition into a single NDTM, which can also be run. Hence, there is a direct correspondence between propositions about programs (e.g., the program returns its input sorted) and NDTMs. Hence, you can most certainly run a proposition about programs (though perhaps not all propositions). The temporal logic of actions (TLA) is a complete logic in the sense that for every NDTM (or a DTM as a special case) there exists a (non-unique) TLA expression, consisting of the simple logical connectives, the priming operator (an action) and possibly LTL operators (describing say, fairness, properties) that describes that particular TM. But, of course, a TLA expression can be less precise, and describe a whole set of TMs -- a proposition. Therefore in TLA, propositions and programs are the same object. Here's Lamport in the opening paragraph introducing TLA in the 1993 paper[1]: Correctness of [an] algorithm means that the program satisfies a desired property. We propose a simpler approach in which both the algorithm and the property are specified by formulas in a single logic. Correctness of the algorithm means that the formula specifying the algorithm implies the formula specifying the property, where implies is ordinary logical implication. FYI, that paper has 2458 citations and is far from obscure. This theory is much better known in the software verification community than type theory (certainly when you consider it within the greater framework of temporal logics, of which TLA is one), and has had a greater impact -- both academic and real-world -- on formal methods, at least so far. Specifying programs as propositions in temporal logics was a modern theoretical turning point in CS, and has yielded two or three Turing awards (Pnueli in '96, Clarke et al. in '07, and Lamport -- at least partly for this -- in '13). > Even if I charitably interpret that as “decide its truth value”, well, not all propositions are decidable! This is where things are a bit tricky. For a complete treatment see the preliminaries section in this '88 paper by Abadi and Lamport[2]. > A proposition has a truth value - a proof does not. Of course, but there's room for interpretation here (like I said, I'm not a type expert so I'm not 100% sure about it): `<x = 3, y = 5>` can be viewed as a proof object of the proposition `∃x,y ∈ 1..10 . x < y`, but it can also be viewed as the more precise proposition, `x = 3 ∧ y = 5`. Existential propositions (or types) can therefore be viewed as a set of multiple programs, while the proof object is a particular program, that could have been specified with a more precise proposition. That is what I meant when I said "hidden proposition". If you step back from typed LC and consider the original proof objects, those objects are just a series (a tree, actually) of logical deductions. Each of those deductions is a proposition. A proof is, therefore, a series of true propositions, each derived from the previous one using one of the deduction rules. You can certainly say, then, that a proof is a collection of hidden (true) propositions. [1]: http://research.microsoft.com/pubs/64074/lamport-actions.pdf http://research.microsoft.com/pubs/64074/lamport-actions.pdf [2]: http://research.microsoft.com/pubs/64046/abadi-existence.pdf http://research.microsoft.com/pubs/64046/abadi-existence.pdf