3 ms·

>> 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 the

>> 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
    > 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? Theoretically, you can verify the program itself in TLA+, in a manner similar to how seL4 verified their code. You compile your final code to TLA+ to produce a low-level spec that captures the actual semantics of your progam, and check that it is a refinement of your high-level spec. Research teams have done this for Java and C (http://tla2014.loria.fr/slides/methni.pdf http://tla2014.loria.fr/slides/methni.pdf). The problem is that it doesn't scale, and neither does any other form of end-to-end proof. Humanity has never been able to formally prove an actual program that is anywhere near what we would call "large". The reason you'd bother doing it is that 1. unlike end-to-end verification it is not only affordable, but also reduces costs, and 2. it actually works in uncovering the most costly problems, as verified by years of experience in industry on large projects. > The program can be generated from the specification. Ah, that is an interesting research question. Obviously in some cases a program could be generated. The spec would need to be deterministic for one (or nondeterministic in a way that makes sense for an actual program, like when representing multiple processes), computable (you can easily specify a program that takes an arbitrary program as input and says, "in the first step, let x be equal to TRUE if the input program terminates on the input 13, and FALSE otherwise"), and pretty low level because you can easily write things that would be extremely inefficient to run (like "let x be the smallest prime that's the sum of three squares" or something). Lamport believes that it may be possible (for a properly amenable spec) using machine learning. But it's not like compiling any high-level programming language. > It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification. Research doesn't seem to indicate that it would be, or rather, even if it is a lot more cost effective, it is still beyond affordable for all but high-assurance software, and high-assurance software already makes use of such languages (SCADE and SPARK work very well). But even in high-assurance, the industry doesn't bother with deductive proofs, as model checkers are automatic and work where they're most needed (SCADE) and SMT solvers are also reported to be effective for very restrictive languages (SPARK, but I've never tried it). Manual deductive proofs are used sparingly, to tie together results from automatic verification processes: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h...

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
  > 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? Theoretically, you can verify the program itself in TLA+, in a manner similar to how seL4 verified their code. You compile your final code to TLA+ to produce a low-level spec that captures the actual semantics of your progam, and check that it is a refinement of your high-level spec. Research teams have done this for Java and C (http://tla2014.loria.fr/slides/methni.pdf http://tla2014.loria.fr/slides/methni.pdf). The problem is that it doesn't scale, and neither does any other form of end-to-end proof. Humanity has never been able to formally prove an actual program that is anywhere near what we would call "large". The reason you'd bother doing it is that 1. unlike end-to-end verification it is not only affordable, but also reduces costs, and 2. it actually works in uncovering the most costly problems, as verified by years of experience in industry on large projects. > The program can be generated from the specification. Ah, that is an interesting research question. Obviously in some cases a program could be generated. The spec would need to be deterministic for one (or nondeterministic in a way that makes sense for an actual program, like when representing multiple processes), computable (you can easily specify a program that takes an arbitrary program as input and says, "in the first step, let x be equal to TRUE if the input program terminates on the input 13, and FALSE otherwise"), and pretty low level because you can easily write things that would be extremely inefficient to run (like "let x be the smallest prime that's the sum of three squares" or something). Lamport believes that it may be possible (for a properly amenable spec) using machine learning. But it's not like compiling any high-level programming language. > It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification. Research doesn't seem to indicate that it would be, or rather, even if it is a lot more cost effective, it is still beyond affordable for all but high-assurance software, and high-assurance software already makes use of such languages (SCADE and SPARK work very well). But even in high-assurance, the industry doesn't bother with deductive proofs, as model checkers are automatic and work where they're most needed (SCADE) and SMT solvers are also reported to be effective for very restrictive languages (SPARK, but I've never tried it). Manual deductive proofs are used sparingly, to tie together results from automatic verification processes: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h...