4 ms·

> 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

by 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.

by pron 7y ago

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.