7 ms·

> In practice, we don't do it. There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the proble

> In practice, we don't do it. There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem. Is it really true that TLA scales to large programs? Why isn't there a Compcert in TLA? Why isn't there a Flyspec in TLA? And how about stuff like CertiGrad, where just the spec is pretty involved? My impression has always been that Coq/HOL scale and TLA-style systems break down once your spec gets big enough (let alone the impl).

pron 7y ago
> There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem. The largest programs ever verified end-to-end with Coq, Isabelle, or any other proof assistant correspond to about ~10KLOC of C, or less than 1/5 of jQuery (although such a small program could require up to 50K or even 100K lines of proofs). And even those certainly-non-trivial-yet-rather-tiny programs took years of efforts by experts. Moreover, concessions in the programs' design and choice of algorithms had to be made in order to make verification feasible at all. And I agree that extraction doesn't suffer from a scalability problem. What does is the ability to verify the spec in the first place. If we could write proofs that correspond to programs with 100K, then extracting an executable would not be the isse, but we can't (or, at least, we don't know how). > Is it really true that TLA scales to large programs? Yes. Again, there's no magic: we can only verify so many lines of a formal spec (of which code is an example). So it's either a small program or a small high-level spec that corresponds to a large program. No known technique can affordably verify large (or even medium, or even non-small) programs, end-to-end, for arbitrary functional correctness properties. > Why isn't there a Compcert in TLA? There are programs fifty times the size of CompCert that used TLA+ (to be honest, most real-world programs are 50x the size of CompCert), but not for end-to-end verification; i.e. there is an informal translation of spec to code. Unlike Coq, which is usually used for research or by researchers, TLA+ is used in industry and by "ordinary" engineers without lengthy training in formal logic, so there aren't many papers written about its use, but here's one[1]. Ironically, another reason you don't see as many papers about verification in TLA+ as in Coq is that its use is much simpler. I once saw a paper about specifying and verifying a program's time-complexity in Coq. No one would ever write such a paper about TLA+, because it's just too easy; a TLA+ beginner could do it in their first week of learning (the main reason there's a paper about using TLA+ for PharOS is because they used TLAPS, the TLA+ proof assistant, rather than the TLC model checker, which made the work academically interesting). In any event, if someone is interested in using any of those tools "in production," I recommend they give them all a try. [1]: https://members.loria.fr/SMerz/papers/abz2016-pharos.html https://members.loria.fr/SMerz/papers/abz2016-pharos.html
- throwawayjava 7y ago
  Thanks, that's clarifying. You can do this sort of "lightweight" verification in basically any theorem prover. The difference you observe sounds like a difference in community emphasis rather than capability?
  - pron 7y ago
    There is one big difference in tooling: Coq doesn't have a good model checker. While you can verify several thousand lines of code/spec, writing proofs for those could take months or years, while model-checking is pretty much pushing a button (and then letting the computer or cluster work, possibly for hours or even days), and you probably need to do this a few times, but the difference between having a model checker and not is often the difference between practically reasonable and not. TLA+ has a proof assistant, but people who use TLA+ in industry hardly ever use it because the small added confidence is simply not worth so much more work.
dwohnitmok 7y ago
TLA+ does have things that make it hard for you to modularize and reuse pieces of it in the large. The first category of problems deal with tooling. TLA+ doesn't have a great story when it comes to automation. There is no package manager. Version control is trickier than it needs to be (it's not obvious what files you might want to commit to git and which you shouldn't when you first start working with TLA+). There isn't a lot of support for automatically running things at the commandline (the community mostly uses the TLA+ toolbox, which is a GUI-based IDE). You can and people do these things, but they feel like distinctly second-class citizens. Really TLA+ feels tied to the TLA+ toolbox, warts and all. The second problem is language support. TLA+'s main way of breaking down problems into modules and then using one module as an interface for another (its notion of refinement) suffers from problems analogous to the ones faced when dealing with inheritance. In TLA+'s case, it is easy to add additional new states into a state machine defined in another module (this is TLA+'s celebrated idea of stuttering), but is rather more annoying to do the opposite, e.g. show that in your new module a single state is meant to correspond to a two states in another module (e.g. you have a transaction primitive that allows you to assume that two states can be done simultaneously). This is complicated by the fact that the easiest verification technique in TLA+ is model-checking, which fares the worst when dealing with transitive chains of logical implication. TLA+'s model checker does not have a native notion of logical implication. Instead the way you e.g. prove the statement A => B is by effectively proving A and B but privileging A to be the search space that the model checker operates in. This means chains of the form A => B, B => C, C => D and therefore A => D (and all the intermediate stages) are somewhat annoying. You either prove each step with separate models along the chain and just let a human infer that this means A => D, or you prove the statement A => (B and C and D), without using any of the intermediate implications. Without robust support for transitive implication, the option of using composition in the traditional composition vs. inheritance debate becomes much less palatable as an option when it comes to inheritance. To some extent this is a limitation inherent in model checking and goes away with the proof based verifier for TLA+ TLAPS. But there isn't a collection, that I know of, of proved theorems for TLAPS like many other theorem provers. I suspect again this is due to both the lack of a package manager in the TLA+ ecosystem as well as some not so ergonomic parts of TLAPS. TLAPS feels very magical. Its main way of proving things is what's often referred to as sledgehammer or auto in other theorem provers; write the next step in your proof and hope the computer is smart enough to infer it from the previous step. It feels magical when it works. When the computer can't figure something out, it can be a huge pain to figure out why. It doesn't feel like I'm mechanically building up a proof so much as it feels like I'm playing a guessing game with the computer to see which leaps of logic it'll accept. This gets better with time as you develop an intuition of which leaps work and which don't, but can still be painful. This is mainly because TLAPS itself isn't a prover, but rather delegates to the "magic" methods of other provers. Finally set theory and first order logic, the theoretical basis of TLA+, sometimes makes showing equivalence between items (which is vitally necessary when dealing with code written by multiple individuals who might use different encodings for the same idea) very difficult. In particular, trying to use the fact that A is equivalent to B, therefore some predicate P has an exactly analogous P' on B is tricky. Another way of stating this is that TLA+ as a language makes it a bit difficult to leverage isomorphisms and homomorphisms to reduce the amount of work you have to do. This is somewhere where alternative logical systems can have a big leg up. All that being said, among the technologies commonly referred to as "formal verification," I would say that TLA+ is the one I would most commonly recommend to people in business situations. This precisely because of what many people view as a flaw, that TLA+ is a formal specification language and not a way to actually write or verify actual running code. Because TLA+ specs are divorced from your codebase, they require far less buy-in to see dividends. You don't have to rewrite your codebase in another language. You don't even have to change your coding practices. Indeed TLA+'s closest competitor on most teams is also precisely what most teams lack, which is high-quality documentation. This means you can integrate TLA+ into your work with extremely little risk. Try formalizing your mental model in TLA+. See if it reveals interesting conclusions. If it does, congratulations! TLA+ has been useful to you and you can keep it around as an artifact detailing your thoughts in the future. If not, delete your specs and no harm no foul. No code depends on its existence. You don't need some lengthy transition period to migrate systems away from "using" TLA+. You lose no more time than the amount you put into writing your spec.

pron 7y ago

> There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem. The largest programs ever verified end-to-end with Coq, Isabelle, or any other proof assistant correspond to about ~10KLOC of C, or less than 1/5 of jQuery (although such a small program could require up to 50K or even 100K lines of proofs). And even those certainly-non-trivial-yet-rather-tiny programs took years of efforts by experts. Moreover, concessions in the programs' design and choice of algorithms had to be made in order to make verification feasible at all. And I agree that extraction doesn't suffer from a scalability problem. What does is the ability to verify the spec in the first place. If we could write proofs that correspond to programs with 100K, then extracting an executable would not be the isse, but we can't (or, at least, we don't know how). > Is it really true that TLA scales to large programs? Yes. Again, there's no magic: we can only verify so many lines of a formal spec (of which code is an example). So it's either a small program or a small high-level spec that corresponds to a large program. No known technique can affordably verify large (or even medium, or even non-small) programs, end-to-end, for arbitrary functional correctness properties. > Why isn't there a Compcert in TLA? There are programs fifty times the size of CompCert that used TLA+ (to be honest, most real-world programs are 50x the size of CompCert), but not for end-to-end verification; i.e. there is an informal translation of spec to code. Unlike Coq, which is usually used for research or by researchers, TLA+ is used in industry and by "ordinary" engineers without lengthy training in formal logic, so there aren't many papers written about its use, but here's one[1]. Ironically, another reason you don't see as many papers about verification in TLA+ as in Coq is that its use is much simpler. I once saw a paper about specifying and verifying a program's time-complexity in Coq. No one would ever write such a paper about TLA+, because it's just too easy; a TLA+ beginner could do it in their first week of learning (the main reason there's a paper about using TLA+ for PharOS is because they used TLAPS, the TLA+ proof assistant, rather than the TLC model checker, which made the work academically interesting). In any event, if someone is interested in using any of those tools "in production," I recommend they give them all a try. [1]: https://members.loria.fr/SMerz/papers/abz2016-pharos.html https://members.loria.fr/SMerz/papers/abz2016-pharos.html

throwawayjava 7y ago
Thanks, that's clarifying. You can do this sort of "lightweight" verification in basically any theorem prover. The difference you observe sounds like a difference in community emphasis rather than capability?
- pron 7y ago
  There is one big difference in tooling: Coq doesn't have a good model checker. While you can verify several thousand lines of code/spec, writing proofs for those could take months or years, while model-checking is pretty much pushing a button (and then letting the computer or cluster work, possibly for hours or even days), and you probably need to do this a few times, but the difference between having a model checker and not is often the difference between practically reasonable and not. TLA+ has a proof assistant, but people who use TLA+ in industry hardly ever use it because the small added confidence is simply not worth so much more work.

dwohnitmok 7y ago

TLA+ does have things that make it hard for you to modularize and reuse pieces of it in the large. The first category of problems deal with tooling. TLA+ doesn't have a great story when it comes to automation. There is no package manager. Version control is trickier than it needs to be (it's not obvious what files you might want to commit to git and which you shouldn't when you first start working with TLA+). There isn't a lot of support for automatically running things at the commandline (the community mostly uses the TLA+ toolbox, which is a GUI-based IDE). You can and people do these things, but they feel like distinctly second-class citizens. Really TLA+ feels tied to the TLA+ toolbox, warts and all. The second problem is language support. TLA+'s main way of breaking down problems into modules and then using one module as an interface for another (its notion of refinement) suffers from problems analogous to the ones faced when dealing with inheritance. In TLA+'s case, it is easy to add additional new states into a state machine defined in another module (this is TLA+'s celebrated idea of stuttering), but is rather more annoying to do the opposite, e.g. show that in your new module a single state is meant to correspond to a two states in another module (e.g. you have a transaction primitive that allows you to assume that two states can be done simultaneously). This is complicated by the fact that the easiest verification technique in TLA+ is model-checking, which fares the worst when dealing with transitive chains of logical implication. TLA+'s model checker does not have a native notion of logical implication. Instead the way you e.g. prove the statement A => B is by effectively proving A and B but privileging A to be the search space that the model checker operates in. This means chains of the form A => B, B => C, C => D and therefore A => D (and all the intermediate stages) are somewhat annoying. You either prove each step with separate models along the chain and just let a human infer that this means A => D, or you prove the statement A => (B and C and D), without using any of the intermediate implications. Without robust support for transitive implication, the option of using composition in the traditional composition vs. inheritance debate becomes much less palatable as an option when it comes to inheritance. To some extent this is a limitation inherent in model checking and goes away with the proof based verifier for TLA+ TLAPS. But there isn't a collection, that I know of, of proved theorems for TLAPS like many other theorem provers. I suspect again this is due to both the lack of a package manager in the TLA+ ecosystem as well as some not so ergonomic parts of TLAPS. TLAPS feels very magical. Its main way of proving things is what's often referred to as sledgehammer or auto in other theorem provers; write the next step in your proof and hope the computer is smart enough to infer it from the previous step. It feels magical when it works. When the computer can't figure something out, it can be a huge pain to figure out why. It doesn't feel like I'm mechanically building up a proof so much as it feels like I'm playing a guessing game with the computer to see which leaps of logic it'll accept. This gets better with time as you develop an intuition of which leaps work and which don't, but can still be painful. This is mainly because TLAPS itself isn't a prover, but rather delegates to the "magic" methods of other provers. Finally set theory and first order logic, the theoretical basis of TLA+, sometimes makes showing equivalence between items (which is vitally necessary when dealing with code written by multiple individuals who might use different encodings for the same idea) very difficult. In particular, trying to use the fact that A is equivalent to B, therefore some predicate P has an exactly analogous P' on B is tricky. Another way of stating this is that TLA+ as a language makes it a bit difficult to leverage isomorphisms and homomorphisms to reduce the amount of work you have to do. This is somewhere where alternative logical systems can have a big leg up. All that being said, among the technologies commonly referred to as "formal verification," I would say that TLA+ is the one I would most commonly recommend to people in business situations. This precisely because of what many people view as a flaw, that TLA+ is a formal specification language and not a way to actually write or verify actual running code. Because TLA+ specs are divorced from your codebase, they require far less buy-in to see dividends. You don't have to rewrite your codebase in another language. You don't even have to change your coding practices. Indeed TLA+'s closest competitor on most teams is also precisely what most teams lack, which is high-quality documentation. This means you can integrate TLA+ into your work with extremely little risk. Try formalizing your mental model in TLA+. See if it reveals interesting conclusions. If it does, congratulations! TLA+ has been useful to you and you can keep it around as an artifact detailing your thoughts in the future. If not, delete your specs and no harm no foul. No code depends on its existence. You don't need some lengthy transition period to migrate systems away from "using" TLA+. You lose no more time than the amount you put into writing your spec.