4 ms·

This is really cool! Seeing more examples of formal verification in the wild is always exciting for me. I'm slightly let down by how they are formally proving

This is really cool! Seeing more examples of formal verification in the wild is always exciting for me. I'm slightly let down by how they are formally proving time complexity bounds. I was excited because proving performance bounds is a pretty tough nut to crack, but looking through the sort algorithms (and their overview in Section 1.5) it looks like they don't prove the runtime of the function directly. Rather they create a whole new cost function, assert without proof that the cost function accurately represents the original function, and then prove that the cost function has certain bounds. I would be interested to hear if anyone has experience with formal verification frameworks that can be used to prove time and space complexity bounds of arbitrary code.

throwaway81523 5y ago
A typical way to prove an algorithm uses less than N steps is include N as a "fuel" parameter to the algorithm and decrement it by 1 at each recursive call, so if N reaches 0 then the algorithm has run "out of gas" so it fails. Then you need some proof terms to verify that N never reaches 0. Space complexity is different and functional programming historically hasn't paid such close attention to it, since running out of memory can be seen as an external event like a hardware crash. In other words, idk ;). You might also like Concrete Semantics, a related book: http://concrete-semantics.org/ http://concrete-semantics.org/
- dwohnitmok 5y ago
  Yeah I've heard of the fuel param (although I've only ever used fuel params as a hack to brute force "prove" termination). I'm interested in whether there are frameworks that don't require you to change the function signature. I've skimmed (very very quickly) through Concrete Semantics in the past, but never actually sat down to read it. Does it have anything on proving time or space complexity?
  - throwaway81523 5y ago
    Concrete Semantics is yet another book that looks very good that I want to read someday but haven't. So I don't know if it says anything about either time or space complexity. I believe I learned about using a fuel parameter in an old Edward Yang blog post (http://ezyang.com/ http://ezyang.com/) but I don't have a direct link. Jeff Okasaki's well known book "Purely Functional Data Structures" (highly recommended) does some complexity analyses of operations on functional data structures. They're not formalized but maybe they could be.
    - nextos 5y ago
      I've read and worked through Concrete Semantics and I cannot recall any complexity proofs. It's mostly about program semantics, static analysis, abstract interpretation and type/effect systems.
    - amw-zero 5y ago
      I’m finishing up Concrete Semantics right now. No mention of time complexity that I saw, but even without that it’s become one of my top programming books of all time.
tomsmeding 5y ago
Try playing with Why3. http://why3.lri.fr/ http://why3.lri.fr/ It's slightly idiosyncratic, and it has its own programming language that is ML-like. But it allows you to write arbitrary code in that language, and then prove statements about that code using SMT solvers as helpers. I haven't used it in practice yet, just played with an example, but it felt quite powerful if you get to know its capabilities.
- dwohnitmok 5y ago
  I haven't used Why3, but I have used other SMT solver-based frameworks such as Dafny and TLAPS for TLA+ and they all seem focused on proving function behavior, rather than function runtime or memory usage. I suspect there's a way to encode runtime and memory usage theorems, but I don't have a clear conception of the best way of doing so without polluting function definitions.

throwaway81523 5y ago

A typical way to prove an algorithm uses less than N steps is include N as a "fuel" parameter to the algorithm and decrement it by 1 at each recursive call, so if N reaches 0 then the algorithm has run "out of gas" so it fails. Then you need some proof terms to verify that N never reaches 0. Space complexity is different and functional programming historically hasn't paid such close attention to it, since running out of memory can be seen as an external event like a hardware crash. In other words, idk ;). You might also like Concrete Semantics, a related book: http://concrete-semantics.org/ http://concrete-semantics.org/

dwohnitmok 5y ago
Yeah I've heard of the fuel param (although I've only ever used fuel params as a hack to brute force "prove" termination). I'm interested in whether there are frameworks that don't require you to change the function signature. I've skimmed (very very quickly) through Concrete Semantics in the past, but never actually sat down to read it. Does it have anything on proving time or space complexity?
- throwaway81523 5y ago
  Concrete Semantics is yet another book that looks very good that I want to read someday but haven't. So I don't know if it says anything about either time or space complexity. I believe I learned about using a fuel parameter in an old Edward Yang blog post (http://ezyang.com/ http://ezyang.com/) but I don't have a direct link. Jeff Okasaki's well known book "Purely Functional Data Structures" (highly recommended) does some complexity analyses of operations on functional data structures. They're not formalized but maybe they could be.
  - nextos 5y ago
    I've read and worked through Concrete Semantics and I cannot recall any complexity proofs. It's mostly about program semantics, static analysis, abstract interpretation and type/effect systems.
  - amw-zero 5y ago
    I’m finishing up Concrete Semantics right now. No mention of time complexity that I saw, but even without that it’s become one of my top programming books of all time.

tomsmeding 5y ago

Try playing with Why3. http://why3.lri.fr/ http://why3.lri.fr/ It's slightly idiosyncratic, and it has its own programming language that is ML-like. But it allows you to write arbitrary code in that language, and then prove statements about that code using SMT solvers as helpers. I haven't used it in practice yet, just played with an example, but it felt quite powerful if you get to know its capabilities.

dwohnitmok 5y ago
I haven't used Why3, but I have used other SMT solver-based frameworks such as Dafny and TLAPS for TLA+ and they all seem focused on proving function behavior, rather than function runtime or memory usage. I suspect there's a way to encode runtime and memory usage theorems, but I don't have a clear conception of the best way of doing so without polluting function definitions.