4 ms·

Non click-bait title: "Using Coq to write formal proofs of an image browsing app written in Haskell" While this seems interesting, in this type of application

by throwaway2016a 9y ago

Non click-bait title: "Using Coq to write formal proofs of an image browsing app written in Haskell" While this seems interesting, in this type of application what benefit does this have over, say... unit and integration testing?

MichaelBurge 9y ago
My original motivation for exploring Coq was that I was working on a compiler that repeatedly applied passes until the syntax tree stopped changing. I added some mutable state(like a dirty bit and other things) for performance, and ended up with a few bugs that were hard to track down. One of them was that the compiler would enter an infinite loop because the syntax tree wasn't getting any less complex, but did keep changing. I didn't need any tests, because just running it demonstrated the problem. And it depended on a fairly complex interplay between many passes, so trying to individually test all the permutations would be fragile. I ended up writing a heavy-handed consistency checks that were run after every tiny update, and a tool for searching a verbose reduction log. But I made a note to later see if it was feasible to integrate termination proofs, which seemed like a useful debugging technique that I hadn't tried. I didn't want an article on compilers, because everyone already uses Haskell and Coq to write compilers, so that topic has been done-to-death already. Plus, I figured this would make it seem more approachable. In practice, you should probably just use Rails or something for your webapps.
- tjingrant 9y ago
  Hi, have you ever tried assigning a total order to your syntax tree? Very much like problems occurring in Buchberger's algorithm and its generalized form Knuth-Bendix completion; they have a very sophisticated way of recursively assigning weights to each term (which there can be infinitely many).
noblethrasher 9y ago
A computer, being approximately a Universal Turing Machine, can virtualize anything, including a "better" computer. So, a better question to ask is: "If unit and integration testing are so great, why not create a virtual system and corresponding programming language that will do nearly all of the unit and integration testing automatically."
- mdpopescu 9y ago
  I believe Microsoft's Pex [1] is an attempt to generate all the unit tests automatically. You can't do that with integration tests, because their number grows exponentially with the number of paths in the code [2]. [1] https://www.microsoft.com/en-us/research/project/pex-and-moles-isolation-and-white-box-unit-testing-for-net/ https://www.microsoft.com/en-us/research/project/pex-and-mol... [2] http://blog.thecodewhisperer.com/permalink/integrated-tests-are-a-scam http://blog.thecodewhisperer.com/permalink/integrated-tests-...
logicchains 9y ago
>While this seems interesting, in this type of application what benefit does this have over, say... unit and integration testing? It provides infinitely more assurance than any amount of unit/integration testing: it guarantees that the application behaves as specified, which guarantees correctness if the spec is correct (and if the spec is not correct, then testing won't help either). It also turns what's possibly the least enjoyable part of software development into the most enjoyable part.
- yodsanklai 9y ago
  > It provides infinitely more assurance than any amount of unit/integration testing I would say it's complementary. There are sources of error that you don't capture in the formal model so you can't skip the test. The question is whether it's worth spending this verification effort for such an application. How much more confidence do you get, how much did you spend for it, and did you really need it? > if the spec is not correct, then testing won't help either I think that you can detect bugs in your spec when testing.
  - johncolanduoni 9y ago
    > I think that you can detect bugs in your spec when testing. It's worth noting that when you construct and prove hypotheses in mathematics you will almost always go through an initial phase of spot testing good examples/counter-examples before you attempt a proof. So these methods are still very complementary even when you turn the abstractness up to 11.
  - WarDaft 9y ago
    Actually that's not true. Now that we have Phantheck, all QuickCheck tests (which are a very pleasant superclass of unit tests) can just be lifted to the type level with TH magic. This makes them dramatically more useful. This is because you cannot traditionally write a function that requires that its arguments pass some test, but you can write a function that requires they have a certain type. But now you can require arbitrary QuickCheck-able properties via types. Note that you can still capture any property you want via non-metaprogramming types (though you may require a trusted kernel to keep things performant) but that can be trickier to work with than a test for people who are much more accustomed to tests than types. Also note that writing a function that should work, but won't typecheck can also reveal a flaw in the model (or in what you thought the model should be, or in what kind of operations you thought should work)
tluyben2 9y ago
It is a question of completeness; the proof your provide must be complete for your case while your unit tests do not have to be. What you want is that your code does what you intend to do and in languages like Coq, Idris and f* you have to provide a proof for it that covers not some subset fuzzing test (or physics) proof but a full covering (or math) proof. Simplified and this is a subject of a lot of CS research as we know it is needed. Before I insult anyone who studied physics; the above idea that physics just tries something 1000 times and then considers it true while math makes it all covering is a thing Dijkstra used to say when teaching at TUE in Eindhoven NL and I always remembered it as it is empirical vs math. I use the much lighter TLA+ myself as indeed only(?) French rail pays for actual formal verification in software.
- mjburgess 9y ago
  A total aside here, but this Humean view of science isn't really accurate, though often repeated. It isnt that something happens 1000x. It's that we arrive at a causal explanation of how something happens and then this explanation is confirmed across 1000 instances, so on the basis of this causal explanation being accurate enough, it is reasonable to predict the 1001. The difference is that in the Humean "1000x therefore 1001" case there is no reason to suppose 1001. If the world were really just these sequences it would be inexplicable. Rather, the world has a causal structure and it this that we better understand by making inferences. cf. induction vs. abduction
lostmsu 9y ago
> While this seems interesting, in this type of application what benefit does this have over, say... unit and integration testing? There were numerous remote code execution exploits caused by improper image handling libraries. So I can see quite a value in a verified image manipulation tool.

MichaelBurge 9y ago

My original motivation for exploring Coq was that I was working on a compiler that repeatedly applied passes until the syntax tree stopped changing. I added some mutable state(like a dirty bit and other things) for performance, and ended up with a few bugs that were hard to track down. One of them was that the compiler would enter an infinite loop because the syntax tree wasn't getting any less complex, but did keep changing. I didn't need any tests, because just running it demonstrated the problem. And it depended on a fairly complex interplay between many passes, so trying to individually test all the permutations would be fragile. I ended up writing a heavy-handed consistency checks that were run after every tiny update, and a tool for searching a verbose reduction log. But I made a note to later see if it was feasible to integrate termination proofs, which seemed like a useful debugging technique that I hadn't tried. I didn't want an article on compilers, because everyone already uses Haskell and Coq to write compilers, so that topic has been done-to-death already. Plus, I figured this would make it seem more approachable. In practice, you should probably just use Rails or something for your webapps.

tjingrant 9y ago
Hi, have you ever tried assigning a total order to your syntax tree? Very much like problems occurring in Buchberger's algorithm and its generalized form Knuth-Bendix completion; they have a very sophisticated way of recursively assigning weights to each term (which there can be infinitely many).

noblethrasher 9y ago

A computer, being approximately a Universal Turing Machine, can virtualize anything, including a "better" computer. So, a better question to ask is: "If unit and integration testing are so great, why not create a virtual system and corresponding programming language that will do nearly all of the unit and integration testing automatically."

mdpopescu 9y ago
I believe Microsoft's Pex [1] is an attempt to generate all the unit tests automatically. You can't do that with integration tests, because their number grows exponentially with the number of paths in the code [2]. [1] https://www.microsoft.com/en-us/research/project/pex-and-moles-isolation-and-white-box-unit-testing-for-net/ https://www.microsoft.com/en-us/research/project/pex-and-mol... [2] http://blog.thecodewhisperer.com/permalink/integrated-tests-are-a-scam http://blog.thecodewhisperer.com/permalink/integrated-tests-...

logicchains 9y ago

>While this seems interesting, in this type of application what benefit does this have over, say... unit and integration testing? It provides infinitely more assurance than any amount of unit/integration testing: it guarantees that the application behaves as specified, which guarantees correctness if the spec is correct (and if the spec is not correct, then testing won't help either). It also turns what's possibly the least enjoyable part of software development into the most enjoyable part.

yodsanklai 9y ago
> It provides infinitely more assurance than any amount of unit/integration testing I would say it's complementary. There are sources of error that you don't capture in the formal model so you can't skip the test. The question is whether it's worth spending this verification effort for such an application. How much more confidence do you get, how much did you spend for it, and did you really need it? > if the spec is not correct, then testing won't help either I think that you can detect bugs in your spec when testing.
- johncolanduoni 9y ago
  > I think that you can detect bugs in your spec when testing. It's worth noting that when you construct and prove hypotheses in mathematics you will almost always go through an initial phase of spot testing good examples/counter-examples before you attempt a proof. So these methods are still very complementary even when you turn the abstractness up to 11.
- WarDaft 9y ago
  Actually that's not true. Now that we have Phantheck, all QuickCheck tests (which are a very pleasant superclass of unit tests) can just be lifted to the type level with TH magic. This makes them dramatically more useful. This is because you cannot traditionally write a function that requires that its arguments pass some test, but you can write a function that requires they have a certain type. But now you can require arbitrary QuickCheck-able properties via types. Note that you can still capture any property you want via non-metaprogramming types (though you may require a trusted kernel to keep things performant) but that can be trickier to work with than a test for people who are much more accustomed to tests than types. Also note that writing a function that should work, but won't typecheck can also reveal a flaw in the model (or in what you thought the model should be, or in what kind of operations you thought should work)

tluyben2 9y ago

It is a question of completeness; the proof your provide must be complete for your case while your unit tests do not have to be. What you want is that your code does what you intend to do and in languages like Coq, Idris and f* you have to provide a proof for it that covers not some subset fuzzing test (or physics) proof but a full covering (or math) proof. Simplified and this is a subject of a lot of CS research as we know it is needed. Before I insult anyone who studied physics; the above idea that physics just tries something 1000 times and then considers it true while math makes it all covering is a thing Dijkstra used to say when teaching at TUE in Eindhoven NL and I always remembered it as it is empirical vs math. I use the much lighter TLA+ myself as indeed only(?) French rail pays for actual formal verification in software.

mjburgess 9y ago
A total aside here, but this Humean view of science isn't really accurate, though often repeated. It isnt that something happens 1000x. It's that we arrive at a causal explanation of how something happens and then this explanation is confirmed across 1000 instances, so on the basis of this causal explanation being accurate enough, it is reasonable to predict the 1001. The difference is that in the Humean "1000x therefore 1001" case there is no reason to suppose 1001. If the world were really just these sequences it would be inexplicable. Rather, the world has a causal structure and it this that we better understand by making inferences. cf. induction vs. abduction

lostmsu 9y ago

> While this seems interesting, in this type of application what benefit does this have over, say... unit and integration testing? There were numerous remote code execution exploits caused by improper image handling libraries. So I can see quite a value in a verified image manipulation tool.