5 ms·

> The full strengths of set theory (sets, functions), plus sugar for sequences and records. Set theory doesn't have any facilities for data abstraction. If any

> The full strengths of set theory (sets, functions), plus sugar for sequences and records. Set theory doesn't have any facilities for data abstraction. If anything, it's the antithesis of data abstraction: every mathematical object (internal to your set theory of choice) is represented as a set (or urelement, but those are even weirder) somehow, even if the encoding is irrelevant for your purposes. > TLA+ has a simple module system. Hierarchical modules? Parameterized module families? Multiple views of the same module, showing or hiding different aspects of it? I use this stuff everyday not only to keep my programs modular, but also to keep their proofs of correctness modular. >> And axiomatic set theories (such as ZF), which are built on top of first-order logic, are definitely not “high-school math”. > None of that has any bearing on specifying algorithms, though. You were the one who originally brought up ZF, describing it as “high-school math”, so I was just refuting that. > That's only because you're used to thinking in a way that is tied to languages. I have yet to encounter a powerful type system as mathematically elegant as TLA+. If elegance is your only criterion, it's very hard to beat Martin-Löf type theory. Of course, usability matters too, and there MLTT fails miserably, at least for programming purposes. Higher-order dependent types don't come for free. > It's done reliably because the properties they represent are kept very computationally simple. That's a feature. It helps you delimit the routine stuff (and can be reliably verified mechanically, and should be most of your program, if it's designed sensibly) from what requires creativity to prove. That being said, of course, existing type systems don't automatically verify everything that could be considered “routine”, so this is an area where further improvement is necessary. > The problem is with more interesting propositions. Prove them by hand. Good old-fashioned brain usage is never going away. --- By the way, I'd like to see your full proof, for the exercise you posted a while back. (“Prove that there exists some i such that y[i] = 1 at the end of the whole computation.”) Is it as short and sweet as my proof?

pron 10y ago
> every mathematical object (internal to your set theory of choice) is represented as a set (or urelement, but those are even weirder) somehow, even if the encoding is irrelevant for your purposes. Yes, but it's completely opaque to a spec. There's no way of obtaining the representation of, say, a function. But let's not get into the debate of set theory pros and cons, because it really makes no difference. > Hierarchical modules? Yes. > Parameterized module families? I don't know what you mean, but you can instantiate the same module multiple times with different parameters. > Multiple views of the same module, showing or hiding different aspects of it? Not that I know of, but as modules are instantiated, you can instantiate them and import, and then export. I can't see this being too useful, though. TLA+ specs are usually small. A 3000 line spec (over multiple modules) is considered very big. > You were the one who originally brought up ZF, describing it as “high-school math”, so I was just refuting that. Those parts of ZF that are used in practice when writing a spec are high school -- sorrt, first-year college -- math. Come on. That people write PhDs on algorithms they implement in Python doesn't mean that Python isn't a high-school-appropriate language. > If elegance is your only criterion, it's very hard to beat Martin-Löf type theory. Actually, it's extremely easy, especially where algorithms are concerned. In TLA, deterministic, nondeterministic, parallel, concurrent, neural, quantum algorithms are all simple special cases, and even better: properties of algorithms and algorithms are the same object. Think of it as type theory with nothing but types, only using ordinary familiar math. That in any type theory a type is a different object from its inhabitants (even if types and programs can use the same terms), already makes it much more complicated than TLA+. > Of course, usability matters too, and there MLTT fails miserably, at least for programming purposes. Higher-order dependent types don't come for free. Right. Amazon, Intel, Oracle and Microsoft engineers use TLA+ all the time to specify and verify very large distributed systems. > Prove them by hand. Good old-fashioned brain usage is never going away. Sure. Except when you have a transactional distributed database algorithm to verify, that's kind of hard. But nobody has the time for deductive proof anyway. TLA+ comes with a model checker. You just press a button and if your assumptions are incorrect you get a counterexample. > By the way, I'd like to see your full proof, for the exercise you posted a while back. (“Prove that there exists some i such that y[i] = 1 at the end of the whole computation.”) Is it as short and sweet as my proof? Shorter and sweeter :) Informally, it goes as follows. This is our partial correctness property PartialCorrectness ≜ AllDone ⇒ ∃ p ∈ ProcSet : y[p] = 1 And this is the inductive invariant: Inv ≜ PartialCorrectness ∧ ∀ p ∈ ProcSet : pc[p] ≠ "Line1" ⇒ x[p] = 1 We need to show that Inv implies PartialCorrectness (trivial), that Inv holds in the initial state, and that if it holds in any state s, then it holds in any possible consecutive step s'. It's easy to see that it holds in the initial state. Now, let's assume it holds in s, and prove for s'. To make this transition, some process p either executes line 1 or executes line 2. If it executes 1, then PartialCorrectness doesn't change because no new process is done. The second conjunct holds because we've just left line 1 and x has been assigned (by the definition of line 1). If we are currently in line 2, the second conjunct of the invariant doesn't change. By the definition of this action, we'll be done. Here we have two cases, either we set y to 1, or we set y to zero. If we set y to 1, we're done and PartialCorrectness holds. If we set y to 0 then by the assumption of the invariant, the process we depend on must not be done, hence AllDone is false, and PartialCorrectness holds. QED. Now, the machine-checked formal proof no longer looks so short and sweet because, well, it's completely formal and verified by a checker, so there's a lot of detail that's absent from an informal proof (I'd like to see you formally explain to a proof assistant: respecting the old interleaving, or even your inductive step). TLA+ proofs are written in Lamport's structured "modern" proof style: http://research.microsoft.com/en-us/um/people/lamport/pubs/proof http://research.microsoft.com/en-us/um/people/lamport/pubs/p... Also, note that I wanted to show this to someone else, and for pedagogical reasons I wrote the program in an imperative language called PlusCal that is then compiled to TLA+. In TLA+, the "program" is the formulas Init and Next. They are combined to form the temporal formula Spec. A non-modal subformula means that the condition holds in the first state of the behavior. A square operator ("always") means that the subformula holds in all suffixes of the behavior (and a diamond means that it eventually holds). The square brackets with the "vars" subscript has to do with stuttering, which is important for composition and refinement, but I won't explain it here. Here is the spec with the formal proof: https://www.dropbox.com/s/7i239785jngat2b/Foo.pdf?dl=0 https://www.dropbox.com/s/7i239785jngat2b/Foo.pdf?dl=0
- catnaroek 10y ago
  >> Multiple views of the same module, showing or hiding different aspects of it? > Not that I know of, but as modules are instantiated, you can instantiate them and import, and then export. I can't see this being too useful, though. TLA+ specs are usually small. So it doesn't scale to entire programs? > A 3000 line spec (over multiple modules) is considered very big. A 3000 line program is fairly small. > Come on. That people write PhDs on algorithms they implement in Python Presumably they don't actually prove things about Python programs directly. If they do, what formal semantics for Python are they using? > doesn't mean that Python isn't a high-school-appropriate language. Formally reasoning about Python programs is a huge pain. Why would anyone want to subject high-schoolers to that? > Informally, it goes as follows. (proof) Okay, it was much shorter and sweeter than I expected. Well done. > TLA+ comes with a model checker. You just press a button and if your assumptions are incorrect you get a counterexample. What I want is proofs, not just truth values. A proof is a syntactic object that can be analyzed, partially reused, combined with other proofs, etc.
  - pron 10y ago
    > A 3000 line program is fairly small. TLA+ is not a programming language. A 3000 line spec easily specifies a 100KLOC program. > What I want is proofs, not just truth values. A proof is a syntactic object that can be analyzed, partially reused, combined with other proofs, etc. Sure, but: 1. if you're wrong, a model checker gives you a counterexample; this is invaluable in understanding what's going on and fixing your bugs. It's much easier to prove something when it's true. 2. Unfortunately, the difference between the cost of deductive proof and running a model checker is at least one if not two orders of magnitude. It is common industry experience (reported most recently by Amazon about TLA+), that a model checker provides the best bang-for-the-buck. It actually reduces development costs overall. Deductive proofs are cost-prohibitive for all but the most well-funded, patient and rather modestly sized programs. They're worth it mostly if you're willing to pay 10x to go from, say, 97% certainty to 99.9%.
    - catnaroek 10y ago
      > TLA+ is not a programming language. A 3000 line spec easily specifies a 100KLOC program. So, which is it? (0) After you verify a TLA+ specification, you still have the rather large task of making sure your actual program satisfies the specification. In this case, why should I bother verifying something that isn't the final program? (1) The program can be generated from the specification. In this case, the TLA+ specification is a program, although it's written in an unusually high-level language. > Deductive proofs are cost-prohibitive for all but the most well-funded, patient and rather modestly sized programs. It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification.

pron 10y ago

> every mathematical object (internal to your set theory of choice) is represented as a set (or urelement, but those are even weirder) somehow, even if the encoding is irrelevant for your purposes. Yes, but it's completely opaque to a spec. There's no way of obtaining the representation of, say, a function. But let's not get into the debate of set theory pros and cons, because it really makes no difference. > Hierarchical modules? Yes. > Parameterized module families? I don't know what you mean, but you can instantiate the same module multiple times with different parameters. > Multiple views of the same module, showing or hiding different aspects of it? Not that I know of, but as modules are instantiated, you can instantiate them and import, and then export. I can't see this being too useful, though. TLA+ specs are usually small. A 3000 line spec (over multiple modules) is considered very big. > You were the one who originally brought up ZF, describing it as “high-school math”, so I was just refuting that. Those parts of ZF that are used in practice when writing a spec are high school -- sorrt, first-year college -- math. Come on. That people write PhDs on algorithms they implement in Python doesn't mean that Python isn't a high-school-appropriate language. > If elegance is your only criterion, it's very hard to beat Martin-Löf type theory. Actually, it's extremely easy, especially where algorithms are concerned. In TLA, deterministic, nondeterministic, parallel, concurrent, neural, quantum algorithms are all simple special cases, and even better: properties of algorithms and algorithms are the same object. Think of it as type theory with nothing but types, only using ordinary familiar math. That in any type theory a type is a different object from its inhabitants (even if types and programs can use the same terms), already makes it much more complicated than TLA+. > Of course, usability matters too, and there MLTT fails miserably, at least for programming purposes. Higher-order dependent types don't come for free. Right. Amazon, Intel, Oracle and Microsoft engineers use TLA+ all the time to specify and verify very large distributed systems. > Prove them by hand. Good old-fashioned brain usage is never going away. Sure. Except when you have a transactional distributed database algorithm to verify, that's kind of hard. But nobody has the time for deductive proof anyway. TLA+ comes with a model checker. You just press a button and if your assumptions are incorrect you get a counterexample. > By the way, I'd like to see your full proof, for the exercise you posted a while back. (“Prove that there exists some i such that y[i] = 1 at the end of the whole computation.”) Is it as short and sweet as my proof? Shorter and sweeter :) Informally, it goes as follows. This is our partial correctness property PartialCorrectness ≜ AllDone ⇒ ∃ p ∈ ProcSet : y[p] = 1 And this is the inductive invariant: Inv ≜ PartialCorrectness ∧ ∀ p ∈ ProcSet : pc[p] ≠ "Line1" ⇒ x[p] = 1 We need to show that Inv implies PartialCorrectness (trivial), that Inv holds in the initial state, and that if it holds in any state s, then it holds in any possible consecutive step s'. It's easy to see that it holds in the initial state. Now, let's assume it holds in s, and prove for s'. To make this transition, some process p either executes line 1 or executes line 2. If it executes 1, then PartialCorrectness doesn't change because no new process is done. The second conjunct holds because we've just left line 1 and x has been assigned (by the definition of line 1). If we are currently in line 2, the second conjunct of the invariant doesn't change. By the definition of this action, we'll be done. Here we have two cases, either we set y to 1, or we set y to zero. If we set y to 1, we're done and PartialCorrectness holds. If we set y to 0 then by the assumption of the invariant, the process we depend on must not be done, hence AllDone is false, and PartialCorrectness holds. QED. Now, the machine-checked formal proof no longer looks so short and sweet because, well, it's completely formal and verified by a checker, so there's a lot of detail that's absent from an informal proof (I'd like to see you formally explain to a proof assistant: respecting the old interleaving, or even your inductive step). TLA+ proofs are written in Lamport's structured "modern" proof style: http://research.microsoft.com/en-us/um/people/lamport/pubs/proof http://research.microsoft.com/en-us/um/people/lamport/pubs/p... Also, note that I wanted to show this to someone else, and for pedagogical reasons I wrote the program in an imperative language called PlusCal that is then compiled to TLA+. In TLA+, the "program" is the formulas Init and Next. They are combined to form the temporal formula Spec. A non-modal subformula means that the condition holds in the first state of the behavior. A square operator ("always") means that the subformula holds in all suffixes of the behavior (and a diamond means that it eventually holds). The square brackets with the "vars" subscript has to do with stuttering, which is important for composition and refinement, but I won't explain it here. Here is the spec with the formal proof: https://www.dropbox.com/s/7i239785jngat2b/Foo.pdf?dl=0 https://www.dropbox.com/s/7i239785jngat2b/Foo.pdf?dl=0

catnaroek 10y ago
>> Multiple views of the same module, showing or hiding different aspects of it? > Not that I know of, but as modules are instantiated, you can instantiate them and import, and then export. I can't see this being too useful, though. TLA+ specs are usually small. So it doesn't scale to entire programs? > A 3000 line spec (over multiple modules) is considered very big. A 3000 line program is fairly small. > Come on. That people write PhDs on algorithms they implement in Python Presumably they don't actually prove things about Python programs directly. If they do, what formal semantics for Python are they using? > doesn't mean that Python isn't a high-school-appropriate language. Formally reasoning about Python programs is a huge pain. Why would anyone want to subject high-schoolers to that? > Informally, it goes as follows. (proof) Okay, it was much shorter and sweeter than I expected. Well done. > TLA+ comes with a model checker. You just press a button and if your assumptions are incorrect you get a counterexample. What I want is proofs, not just truth values. A proof is a syntactic object that can be analyzed, partially reused, combined with other proofs, etc.
- pron 10y ago
  > A 3000 line program is fairly small. TLA+ is not a programming language. A 3000 line spec easily specifies a 100KLOC program. > What I want is proofs, not just truth values. A proof is a syntactic object that can be analyzed, partially reused, combined with other proofs, etc. Sure, but: 1. if you're wrong, a model checker gives you a counterexample; this is invaluable in understanding what's going on and fixing your bugs. It's much easier to prove something when it's true. 2. Unfortunately, the difference between the cost of deductive proof and running a model checker is at least one if not two orders of magnitude. It is common industry experience (reported most recently by Amazon about TLA+), that a model checker provides the best bang-for-the-buck. It actually reduces development costs overall. Deductive proofs are cost-prohibitive for all but the most well-funded, patient and rather modestly sized programs. They're worth it mostly if you're willing to pay 10x to go from, say, 97% certainty to 99.9%.
  - catnaroek 10y ago
    > TLA+ is not a programming language. A 3000 line spec easily specifies a 100KLOC program. So, which is it? (0) After you verify a TLA+ specification, you still have the rather large task of making sure your actual program satisfies the specification. In this case, why should I bother verifying something that isn't the final program? (1) The program can be generated from the specification. In this case, the TLA+ specification is a program, although it's written in an unusually high-level language. > Deductive proofs are cost-prohibitive for all but the most well-funded, patient and rather modestly sized programs. It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification.