Has anyone here ever used Coq to verify a non-trivial piece of production software? What was the experience like? (I have experience with other formal methods, a good amount of TLA+ and tiny a bit of Alloy and Why3, but I've never used Coq)
The LSRA is also extractable as a Haskell library, so they can use it in their compiler:
http://hackage.haskell.org/package/linearscan
From what I understand from John, implementing it was quite a challenge. It's certainly not for the faint of heart, but it is not completely impossible. In any case, they seem to have had success with this project and are moving onto working on other components of the project, from what I can tell.
That said, from my own personal experience, you're probably a lot better off trying to see if you can formulate your problems in a more domain-specific way and leverage tools for that. Full blown general theorem proving is much more difficult, and I try to think of it more as something to resort to if easier approaches don't work.
We still haven't entirely wrapped our heads around the fundamentals like equality (just because it's fundamental doesn't mean it's simple), so there's still a lot of work to be done in the DT world. DTs are one of those cases where I feel the curve is very much exponential: getting 98% of the "correctness" of any given piece of code is actually not that difficult. But going from 98% to 99.9999%, like Coq offers? It's outrageously hard. Sometimes that 1.9999% is absolutely mandatory to have, though (considering CompCert is used in e.g. AirBus/aerospace software, yeah, the extra 1.9999% is possibly vital). For most people, it isn't. Even in Haskell, I tend to stay away from super-advanced type level features, because they can introduce incidental complexity, and Haskell is already somewhere around that 95% mark anyway. With enough type level stuff, it can probably get to about 98%, but with some incidental complexity. So in the vast majority of cases I don't stand to gain much, unless things get extreme...
(And personally, out of any theorem prover, I'm most excited for Lean as opposed to Coq, because I like: its speed, and it has many useful features like directly being able to use it to program through meta definitions and the Lean virtual machine, its API and automation features -- and things like C++ code generation.)
> We still haven't entirely wrapped our heads around the fundamentals like equality (just because it's fundamental doesn't mean it's simple), so there's still a lot of work to be done in the DT world.
Yeah, even though in the end the proof techniques are similar in algorithms that are complex enough (invariants, refinement), I think that DTs in particular add a lot of accidental complexity (but that's because they try to do more than "just" verification). The difficulty of equality is not fundamental to computations -- it's an artifact of the functional formalism...
> But going from 98% to 99.9999%, like Coq offers? It's outrageously hard.
That's absolutely true. Much of the problem has to do with the fact that for 100% you need to do end-to-end verification, which means you must reason about the programming language's syntactic constructs, yet with semantics that still generalize and can be reduced (abstracted) to global properties. That's a tall order.
> I'm most excited for Lean
I'll give it a look. I really enjoy TLAPS, the TLA+ proof assistant, but I'm always interested to see what else is out there.
But I don't really mean that "equality is fundamentally hard to compute because of functional programming" or anything. Rather, it might be the other way around: we haven't given a computational meaning to equality, which is why it's all so bad! It's more about equality is ugly at the moment and this results in some of that incidental complexity that I was talking about. To get rid of that ugliness, adopting equality as a computational thing is powerful! The notions of equivalence vs equals vs isomorphic, etc seem to get weird over time, at least in this amateur's mind. And that's not even getting into the problem that you have to establish "equalities" independent of the theory, which is part of, if not the, whole problem (e.g. in set theory, "a equals b" only makes sense once you establish an outside rule for what "equals" means. In HoTT, "equals" is not defined independently of the theory at all -- its in the same universe, so equality is "computational" on its own, in the sense you can talk about equalities, pass them around, and establish equalities between equalities, etcetera. This leads to the notion of infinity-groupoids, univalence, etc)
Granted, it's not like the entire maths community is scrambling to fix this like the Manhattan project; but the notion of equality-being-hazy seems to be understood, even outside of functional formalisms. It seems to be more of a problem in higher order mathematics, too, which is where the majority of people who care about it work, it seems.
While homotopy type theory is the current en-vogue approach to solving the hairy problems of equality (among other things) since it unifies all this... actually adding a computational interpretation is still an open question. So one problem is solved and another pops up, just as usual...
Perhaps, but not for computation. There is a very clear, very nice, partial order on various kinds of computational semantics, and they all become a nice, "configurable" sliding scale once you work in a formalism that expresses computation more naturally than functions (that's because computations are simply not functions, at least not functions from the input to the output, and not even partial functions). Once you decide to work with functions you need to think of things like extensional vs. intensional equality etc., which simply aren't an issue in other formalisms.
> It seems to be more of a problem in higher order mathematics, too.
True, but the need for "higher-order mathematics" in the modeling of computation in the first place originates with the choice of functions as models of computation...
Consider this: computation bears a lot of resemblance to continuous dynamical systems (computation is essentially a discrete dynamical process). Now, in (continuous) dynamical system, suppose you want to make your system "higher order": the derivative of the system will itself by a dynamical system. There is still no need to go higher-order mathematically; dynamical systems are usually represented as first order ODEs regardless of their conceptual "order". Instead, all you do is add another dimension to your state space. As the size of your state-vector is arbitrary, and as the mathematics of increasing it is very clear, all you need to do to "go deep" is "go wide".
But perhaps I'm being unfair. While functions are not a very good abstraction for reasoning about computation, they are a very useful programming abstraction, and for end-to-end verification you must reason at the programming language level (although there may be better ways of doing that, too).
> True, but the need for higher-order mathematics in the modeling of computation in the first place originates with the choice of functions as models of computation... But perhaps I'm being unfair. While functions are not a very good abstraction for reasoning about computation, they are a very useful programming abstraction, and for end-to-end verification you must reason at the programming language level (although there may be better ways of doing that, too).
I kind of left "higher order mathematics" a bit vague... Personally in all the proofs, etc I've needed you don't need to go as far as talking about topological spaces or n-categories or whatever, which is what I'd consider "higher order", but this is the space where a lot of the focus on wrangling equality, etc seems to come from, which is what I was getting at. Then again, most people using Coq heavily are probably exactly the people who care about this. :) I'm not one of those people, I just like programming.
And personally I find the choice of functions, etc as a notion of computation quite powerful, even if it gets hairy sometimes! I suppose you could call it pidgeon-holing or laziness, but I tend to get a lot of insight from viewing mathematics from a computational, constructive point of view like this. I more use it as a "bridge" to get places rather than an overarching view of mathematics, I suppose, and I think it's quite useful at that (e.g. recently I found that I like the view of quotients in the computational, type-theoretic view rather than the 'quotients' of non-type-theory where you're really talking about partitions and equivalence classes, etc)... This is also probably partially due to the fact I've spent the majority of my programming career with systems like Haskell. So I'm fairly comfortable with "computational mathematics" from this POV.
In other words, I don't think that an interesting way to apply computational concepts (of typed lambda calculus) to the foundations of mathematics is necessarily the best way to apply mathematical thinking to computation. "Computational math" may not be the right math for "mathematical computation". There's an example of this unjustified (although possibly true -- we don't know) reasoning in the introduction to the Lean paper:
> In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point establishing claims as to their correctness becomes a form of theorem proving. Conversely, the proof of a mathematical theorem may require a lengthy computation, in which case verifying the truth of the theorem requires verifying that the computation does what it is supposed to do.
The problem is that the kinds of computations relevant in the first case and the kinds of computation in the second case can be wildly different. Computations used in proofs are very much "functional" (map input to output). Computations in real-world software systems that really need formal verification rarely are. The most common type of computation in either category is the least common in the other, so the assumption that the same mathematical foundation (and/or the same tool) should be used for both is unjustified. While the authors use the term "in practice" to preface their statement, judging by their publication history, I'm a bit skeptical of their experience in verifying real-world software.
Nevertheless, Lean does seem like a great way to learn about dependent types, and as you pointed out, the work on dependent types and their possible application in software verification is far from done, so it's very hard to judge at this point whether or not the direction is the right one. In the end, regardless of formalism, the proofs and techniques of software verification turn out to be very similar in all formalisms.
I know of some small scale use at Facebook (where I work), where it has been used to verify a non-trivial protocol under various combinations of failures.
Whilst it does discuss that Amazon used TLA+ in nontrivial circumstances, it's still a long mental leap to me to get to "TLA+ for AWS S3 looked like this, and this is the sort of bug it helped quash".
It'd be great to see some of that sort of thing.
The kind of bugs you find when verifying distributed systems is, if this machine was in that state and that message was in transit, and then the other machine failed, then data was lost".
Basically, because formal verification of this kind ensures the specification is correct, it will find any kind of bug there is. But it's those bugs that are either a result of a severe flaw in the design, or bugs that would be hard to find in testing but their results may be serious, that make this worthwhile.
It has some objective qualities and some subjective ones. The objective ones (as confirmed by others) are that it's easy to learn and you can get productive very fast. I immediately started specifying the large project after two weeks of going through Lamport's tutorial[1]. The other objecive benefit is that it has a model checker. Deductively verifying such large specifications (while possible) is simply infeasible (or, rather, unaffordable and an overkill) -- regardless of the tool you use.
The subjective benefit is that the conceptual model quickly clicked for me, personally. I've never liked the aesthetics of modeling arbitrary computations as functions, and the TLA formalism handles sequential, concurrent and parallel computations in the same, extremely elegant way (and allows using the same proof technique regardless of the kind of algorithm, if you want to use the proof assistant). It made me understand what computation is, and how different computations relate to one another, a lot better. The concept -- without the technicalities of TLA+ -- is nicely overviewed in [2].
That said, formal methods are never easy because rigorous reasoning about complex algorithms isn't easy, but it beats hunting down bugs (especially in distributed systems) that are very hard to catch and may be catastrophic; it is also very satisfying. I've found TLA+ to add very little "accidental complexity" to this difficult problem.
[1]: https://research.microsoft.com/en-us/um/people/lamport/tla/h...
[2]: https://research.microsoft.com/en-us/um/people/lamport/pubs/...
There's also a Coq framework called Verdi (http://verdi.uwplse.org) for formalizing distributed systems, but I don't know much about it.