5 ms·

A friend of mine used Coq to implement and verify a linear scan register allocator, to be used in the backend of a compiler for his job. He did this on his own

by aseipp 10y ago

A friend of mine used Coq to implement and verify a linear scan register allocator, to be used in the backend of a compiler for his job. He did this on his own over the course of several months, having not known Coq at all beforehand (though he was a Haskell programmer). The LSRA is also extractable as a Haskell library, so they can use it in their compiler: http://hackage.haskell.org/package/linearscan 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.)

pron 10y ago
Thank you! > 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.
- aseipp 10y ago
  Actually, it really seems equality has always been a bit hairy in mathematics, functional programming aside. It's just that trying to formalize it with constructive type theory sort of makes it much more clear how painful it is. :) 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...
  - pron 10y ago
    > The notions of equivalence vs equals vs isomorphic, etc seem to get weird over time 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).

by aseipp 10y ago

pron 10y ago

Thank you! > 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.

aseipp 10y ago
Actually, it really seems equality has always been a bit hairy in mathematics, functional programming aside. It's just that trying to formalize it with constructive type theory sort of makes it much more clear how painful it is. :) 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...
- pron 10y ago
  > The notions of equivalence vs equals vs isomorphic, etc seem to get weird over time 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).