5 ms·

You're asking the wrong question. Unless your program is very small or the property you wish to check is very simple, nothing can fully "validate" it. The quest

by pron 6y ago

You're asking the wrong question. Unless your program is very small or the property you wish to check is very simple, nothing can fully "validate" it. The question should be, is TLA+ more beneficial than just testing in improving program correctness? Humanity currently lacks the means to verify "deep" properties of code at any reasonable scale. Any tool that works at the code level either focuses on very simple properties (memory safety), complex but local properties of a small code-unit (Ada SPARK, Java's OpenJML), or deep properties of tiny programs (like seL4 and CompCert). These can be very important, but none truly offer the ability to "verify code" with some repeatable process at a generally-interesting scale. TLA+ could be used to do the same -- e.g. there is a C to TLA+ compiler -- but then it suffers from the same scale/depth/cost limitation of all code-level tools. So given that we can't just choose to verify a program, the question we want to answer is a different one: what is a good way, in a cost/benefit sense to achieve the correctness we want. Then you can ask whether TLA+ can offer such a way that is "better" in that sense than what you do now, which is likely testing. Those who have tried it, including myself, have come to the conclusion that in cases where the algorithm/design is sufficiently interesting or subtle, the answer is absolutely yes. The way TLA+ achieves it better than code level tools is that it allows you to describe your system at the level appropriate for answering your most important questions about it, and that level can be a much higher one than the code. So, to answer your question, the mere act of precisely expressing your system and correctness criteria in some chosen level of detail using very simple mathematics (high-school or first-year-college level), and then model-checking some interesting instances, is a good way (in the cost/benefit sense) to find bugs and make your program more correct. You compare it to the code by inspection. No, it does not give you 100% guarantees, but nothing else can, either. It is still worthwhile to do in addition to testing, as overall it can easier and cheaper in many cases to detect certain rare-yet-catstrophic bugs. Having said that, there are various techniques being explored that can check whether your program matches the TLA+ specification more mechanically than just by inspection, that might not be sound (i.e. give a 100% guarantee) but increase confidence while being cheap.

zozbot234 6y ago
> Humanity currently lacks the means to verify "deep" properties of code at any reasonable scale. Any tool that works at the code level either focuses on very simple properties (memory safety), complex but local properties of a small code-unit (Ada SPARK, Java's OpenJML), or deep properties of tiny programs (like seL4 and CompCert). This may be true in a sense, but then a TLA+ specification is also a "tiny program" of sorts. There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Even model checking can be subsumed elegantly within such a tool; a model checking run is simply a search for a refutation (as opposed to a positive proof) of some claimed properties wrt. the proposed spec.
- pron 6y ago
  > There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Sure, and that is what TLA+, together with its tools, aim to do. The problem is the relation between the spec, that you can precisely verify, and the program it aims to abstract. The advantage TLA+ has over code-level tools in this respect is that those tools use code as their specification language -- i.e. a formal language that is deterministic enough to efficiently compile/interpret and execute. But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. For example, in TLA+ you can say, suppose I have a subroutine that sorts, and then build and check your specification on top of that without actually writing a sorting routine that can be executed. Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This way, you can write a specification that's small enough to be verified, yet captures the interesting aspects of a system that's made of too much code to verify at the code level.
  - zozbot234 6y ago
    > But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. ... Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This can also be done in many end-to-end tools. Typically, these tools allow for end-to-end proof based on the actual code; they don't require it.
doonesbury 6y ago
While tla+ supports pluscal so the the spec is closer to imperative programming one ultimately would do it's true there is an insuperable gap between the spec and implementation. It should be noted dafny and Verdi are better here. Both systems allow refinement by constantly reproving safety properties over code thats closer and closer to the real implementation including making runnable code. (Verdi does coq to ocaml and dafny does dafny to .net executable generation). Frama C and spark are similar. However there appears to be a philosophical difference: tla+ finds counter examples to the spec. Absence up to the number of states checked shows the code is bug free. Dafny, Verdi seem to proceed by showing the spec is proved through various proof checking (semi) automation. As such they don't explore state. While unit testing and what not has it's place there clear advantage of FM is the developer comes up with the spec first then show/prove it rather than coming up with the spec bug by bug by bug which can be slower and more labor intensive and customer facing. Look if you tell a Dev team we'll need to do four quarters of work over 15 jira epics implemented in two week sprints nobody complains that the plan is dumb because all the requirements aren't really nailed down, the scope could change, or the team might not come up with the algos .. So why even try? But if you tell the same team we'll be using formal methods there's a lot of complaining because FM can't check everything ... Not down to the real final code ... So why bother? I find this dichotomy disingenuous by programmers.
- pron 6y ago
  > It should be noted dafny and Verdi are better here. The problem is that the scale and complexity of systems that are verifiable by Dafny and Verdi, or dozens of not hundreds of other code-level tools, is drastically smaller than those specifiable by TLA+. You are very limited in the scale of the systems you write and verify, and so those tools are much more limited in applicability. It is true that if your program is very small and/or the properties you wish to prove are simple or very specific, then there are tools that can handle them at the code level, and that might be more convenient than TLA+ in those very specific circumstances. Also, Verdi and Dafny are research tools; TLA+ is used in the field by ordinary engineers at Amazon, Microsoft, Oracle, MongoDB and a growing number of other companies to help write software you use quite a lot (most AWS services, for example). > However there appears to be a philosophical difference: tla+ finds counter examples to the spec. Absence up to the number of states checked shows the code is bug free. Dafny, Verdi seem to proceed by showing the spec is proved through various proof checking (semi) automation. As such they don't explore state. That's not the philosophical difference, just a difference in available tooling. Both TLA+ and Dafny are just languages. Both have proof tools that employ SMT solvers for deductive proofs. TLA+ also has a model checker, and perhaps so could Dafny. The philosophical difference is that Dafny is a code-level tool, and so gives you "full cover" but only in limited circumstances, while TLA+ gives you a more partial cover but in a much wider range of use-cases. > But if you tell the same team we'll be using formal methods there's a lot of complaining because FM can't check everything ... Not down to the real final code ... So why bother? I find this dichotomy disingenuous by programmers. I don't know if I'd use the word disingenuous. I think it's just unfamiliarity. The goal of FM tools aimed at "ordinary" software is not to produce perfect software but to eliminate more bugs more cheaply than with tests alone. They shouldn't be compared to a hypothetical perfection, but to what developers use now.
uluyol 6y ago
> Humanity currently lacks the means to verify "deep" properties of code at any reasonable scale. This is an active area of research. Papers are regularly being published (e.g. in the OSDI/SOSP community) that increase the depth or breadth of formal verification. Personally, I don't think we'll ever reach a point where all (or even most) code is formally verified, but it does seem to be making some traction.
lakecresva 6y ago
I think TLA+ is great, but the way in which you try (here and elsewhere) to downplay its inability to verify implementations/executable code by dismissing an OS kernel and an optimizing C compiler as "tiny programs" make you sound like a zealot at best. At worst you sound like a snake-oil salesman when you acknowledge seL4 and CompCert, and then immediately assert that "we can't just choose to verify a program".
- indolering 6y ago
  I'm a big fan of high-assurance code and feel that we should write software as if people's lives depend on it, because they do! But your response is a bit hyperbolic and calling someone a zealot or a snake-oil salesman is in poor taste. CompCert and seL4 represent the upper limit of what can be formally verified, and they are relatively small programs. CompCert targets a subset of C99, which is fairly small. Certainly much smaller than C++ and most other production programming languages. seL4 weighs in at 10K LoC and only provides memory protection and process scheduling. The implementation cost ~2.2 py but the proof cost was ~20 py (although they estimate new tooling would reduce this to ~6 py)[1]. Even Gernot (the head of the seL4 project) stipulates that formal verification is suitable only for software that doesn't change much over time, because it's difficult to add new features without breaking the proof. seL4 benefits from decades of iterations on the L3/L4 design. Now imagine trying to sell formal verification of a product like Gmail, which IIRC has a code base churn of ~20%/year. Even using formal methods to create a markup sanitizer would be a huge research project, probably larger than that of Everest's formally verified implementation of the HTTPS stack[2]. Economies of scale have made commodity programming languages designed for low-assurance code ubiquitous. If we ever want to see investment in high-assurance tooling, we have to prove it's value within the existing marketplace. And we can only do that if we are honest about what is possible and what is profitable. So no, we can't just choose to verify any program. We are getting to the point where it is profitable to formally verify small components, like DNS or the WASM bytecode. That's exciting! But it's not as feasible as you or I want it to be. [1]: https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-... [2]: https://project-everest.github.io/ https://project-everest.github.io/

by pron 6y ago

zozbot234 6y ago

> Humanity currently lacks the means to verify "deep" properties of code at any reasonable scale. Any tool that works at the code level either focuses on very simple properties (memory safety), complex but local properties of a small code-unit (Ada SPARK, Java's OpenJML), or deep properties of tiny programs (like seL4 and CompCert). This may be true in a sense, but then a TLA+ specification is also a "tiny program" of sorts. There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Even model checking can be subsumed elegantly within such a tool; a model checking run is simply a search for a refutation (as opposed to a positive proof) of some claimed properties wrt. the proposed spec.

pron 6y ago
> There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Sure, and that is what TLA+, together with its tools, aim to do. The problem is the relation between the spec, that you can precisely verify, and the program it aims to abstract. The advantage TLA+ has over code-level tools in this respect is that those tools use code as their specification language -- i.e. a formal language that is deterministic enough to efficiently compile/interpret and execute. But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. For example, in TLA+ you can say, suppose I have a subroutine that sorts, and then build and check your specification on top of that without actually writing a sorting routine that can be executed. Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This way, you can write a specification that's small enough to be verified, yet captures the interesting aspects of a system that's made of too much code to verify at the code level.
- zozbot234 6y ago
  > But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. ... Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This can also be done in many end-to-end tools. Typically, these tools allow for end-to-end proof based on the actual code; they don't require it.

doonesbury 6y ago

While tla+ supports pluscal so the the spec is closer to imperative programming one ultimately would do it's true there is an insuperable gap between the spec and implementation. It should be noted dafny and Verdi are better here. Both systems allow refinement by constantly reproving safety properties over code thats closer and closer to the real implementation including making runnable code. (Verdi does coq to ocaml and dafny does dafny to .net executable generation). Frama C and spark are similar. However there appears to be a philosophical difference: tla+ finds counter examples to the spec. Absence up to the number of states checked shows the code is bug free. Dafny, Verdi seem to proceed by showing the spec is proved through various proof checking (semi) automation. As such they don't explore state. While unit testing and what not has it's place there clear advantage of FM is the developer comes up with the spec first then show/prove it rather than coming up with the spec bug by bug by bug which can be slower and more labor intensive and customer facing. Look if you tell a Dev team we'll need to do four quarters of work over 15 jira epics implemented in two week sprints nobody complains that the plan is dumb because all the requirements aren't really nailed down, the scope could change, or the team might not come up with the algos .. So why even try? But if you tell the same team we'll be using formal methods there's a lot of complaining because FM can't check everything ... Not down to the real final code ... So why bother? I find this dichotomy disingenuous by programmers.

pron 6y ago
> It should be noted dafny and Verdi are better here. The problem is that the scale and complexity of systems that are verifiable by Dafny and Verdi, or dozens of not hundreds of other code-level tools, is drastically smaller than those specifiable by TLA+. You are very limited in the scale of the systems you write and verify, and so those tools are much more limited in applicability. It is true that if your program is very small and/or the properties you wish to prove are simple or very specific, then there are tools that can handle them at the code level, and that might be more convenient than TLA+ in those very specific circumstances. Also, Verdi and Dafny are research tools; TLA+ is used in the field by ordinary engineers at Amazon, Microsoft, Oracle, MongoDB and a growing number of other companies to help write software you use quite a lot (most AWS services, for example). > However there appears to be a philosophical difference: tla+ finds counter examples to the spec. Absence up to the number of states checked shows the code is bug free. Dafny, Verdi seem to proceed by showing the spec is proved through various proof checking (semi) automation. As such they don't explore state. That's not the philosophical difference, just a difference in available tooling. Both TLA+ and Dafny are just languages. Both have proof tools that employ SMT solvers for deductive proofs. TLA+ also has a model checker, and perhaps so could Dafny. The philosophical difference is that Dafny is a code-level tool, and so gives you "full cover" but only in limited circumstances, while TLA+ gives you a more partial cover but in a much wider range of use-cases. > But if you tell the same team we'll be using formal methods there's a lot of complaining because FM can't check everything ... Not down to the real final code ... So why bother? I find this dichotomy disingenuous by programmers. I don't know if I'd use the word disingenuous. I think it's just unfamiliarity. The goal of FM tools aimed at "ordinary" software is not to produce perfect software but to eliminate more bugs more cheaply than with tests alone. They shouldn't be compared to a hypothetical perfection, but to what developers use now.

uluyol 6y ago

> Humanity currently lacks the means to verify "deep" properties of code at any reasonable scale. This is an active area of research. Papers are regularly being published (e.g. in the OSDI/SOSP community) that increase the depth or breadth of formal verification. Personally, I don't think we'll ever reach a point where all (or even most) code is formally verified, but it does seem to be making some traction.

lakecresva 6y ago

I think TLA+ is great, but the way in which you try (here and elsewhere) to downplay its inability to verify implementations/executable code by dismissing an OS kernel and an optimizing C compiler as "tiny programs" make you sound like a zealot at best. At worst you sound like a snake-oil salesman when you acknowledge seL4 and CompCert, and then immediately assert that "we can't just choose to verify a program".

indolering 6y ago
I'm a big fan of high-assurance code and feel that we should write software as if people's lives depend on it, because they do! But your response is a bit hyperbolic and calling someone a zealot or a snake-oil salesman is in poor taste. CompCert and seL4 represent the upper limit of what can be formally verified, and they are relatively small programs. CompCert targets a subset of C99, which is fairly small. Certainly much smaller than C++ and most other production programming languages. seL4 weighs in at 10K LoC and only provides memory protection and process scheduling. The implementation cost ~2.2 py but the proof cost was ~20 py (although they estimate new tooling would reduce this to ~6 py)[1]. Even Gernot (the head of the seL4 project) stipulates that formal verification is suitable only for software that doesn't change much over time, because it's difficult to add new features without breaking the proof. seL4 benefits from decades of iterations on the L3/L4 design. Now imagine trying to sell formal verification of a product like Gmail, which IIRC has a code base churn of ~20%/year. Even using formal methods to create a markup sanitizer would be a huge research project, probably larger than that of Everest's formally verified implementation of the HTTPS stack[2]. Economies of scale have made commodity programming languages designed for low-assurance code ubiquitous. If we ever want to see investment in high-assurance tooling, we have to prove it's value within the existing marketplace. And we can only do that if we are honest about what is possible and what is profitable. So no, we can't just choose to verify any program. We are getting to the point where it is profitable to formally verify small components, like DNS or the WASM bytecode. That's exciting! But it's not as feasible as you or I want it to be. [1]: https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-... [2]: https://project-everest.github.io/ https://project-everest.github.io/