7 ms·

Writing a formally-verified image browser in Coq and Haskell

144 points by MichaelBurge 9y ago

sweep4r 9y ago
Writing a porn browser in Coq seems appropriate.
- deleted 9y ago
  [deleted]
- dominotw 9y ago
  do americans call their penis cock/dick and vagina pussy when they are having 'sexytime' ? I find saying 'suck my cock' too immature and comical but at the same time 'suck my penis' sounds too clinical and a mood killer.
  - andai 9y ago
    ayy bb u wan sum penis?
  - wtf_is_up 9y ago
    I prefer to not speak English at all, but to just grunt and make gestures like a chimpanzee.
  - deleted 9y ago
    [deleted]
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-...
lsh 9y ago
+1 - hooray for porn and Haskell
- dang 9y ago
  Would you please stop posting unsubstantive comments to HN? We're trying for higher quality than that and I'm afraid you've been setting a bad example. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
logicchains 9y ago
Did you consider using dependent types to define the image database in such a way that it's impossible to create one that's not InternallyConsistent? This approach can often make proofs shorter/simpler.
- reuben364 9y ago
  Coq isn't very good for developing with properties encoded in the types. Such properties are defined seperately from the data structures involved.
lvkleist 9y ago
this is probably what the creators had in mind when they named the language "coq"
INTPenis 9y ago
Interesting of course but the clickbait title "Porn Browser" made me instantly think of Firefox Focus. I have no idea what build techniques they use but it's definitely a good porn browser in the sense that you can use the family tablet safely and easily with it.
Karrot_Kream 9y ago
Thanks for finally writing an article about Coq that doesn't involve making a compiler. Question: How performant is the generated Haskell code? Also I'd love to see an Idris article next!
- MichaelBurge 9y ago
  Oh, the performance is the worst. Just initializing the database with 6 images ran my 16GB desktop out of memory. I was able to get it running on a 128GB server I have. The root of it seems to be that something somewhere is using Peano naturals rather than binary ones, and the image timestamps are in the billions. So I worked around it by setting all the timestamps to 1: timestamp <- modificationTimeHiRes <$> getFileStatus filepath return $ DB.MkImage DB.N0 filepath (int_to_n 1) If I banned Peano naturals from all Set-level code and used a better extraction library, I don't see why it couldn't be as fast as Haskell. It might also be worth setting the Strict flag on Haskell for the generated code, since Coq seems designed to target ML, which is strict. Anyone have an idea for an Idris article? Maybe "How to make a Bitcoin exchange or Ethereum contract that's 100% guaranteed not to rob you of your money?"
  - iso-8859-1 9y ago
    It's a great idea! Bitcoin needs more formal verification. I wonder how much of e.g. Lightning Network can be proven, assuming SHA256 collisions can't be found, miners include transactions and signatures are unfalsifiable and not malleable. Roasbeef wanted to do it in TLA+, but I am not sure he will find the time.
  - sddfd 9y ago
    Why not use a binary number representation? They are in the library: https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNat.htm https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNa... If you use Z, even the Omega tactic (solver for presburger arithmetic) should work.
    - MichaelBurge 9y ago
ImmatureComment 9y ago
Cock browser lol
- damnfine 9y ago
  You knew these would be downvoted and even made an account name specifically refrencing why. And after all that, a super low effort comment, even for a coq joke. You didn't even try to be humorous or clever... Why bother?
  - mcguire 9y ago
    Sometimes, the effort is its own reward.
tempodox 9y ago
So there is a way to formally verify porn? Theresa May might be interested in that.
- Simon_says 9y ago
  Probably not, since the exact same photo can be classified as porn or not based on the collection of other photos it's grouped with.
- KekDemaga 9y ago
  ”I'll know it when I see it, or when the breast coefficient multiplied by the tumescence index is greater than 9."
nickpsecurity 9y ago
Alright, what I like about this article is it shows the process of specing out the application in a way people new to verification will understand. It's also a useful kind of app instead of a toy language or something. A few critiques follow: " It’s an unspoken truth that most large image databases people have are actually porn collections" Flicker, Tumblr, Imgur, and Facebook Images aren't mostly porn even though one or two are popular for it. So, I doubt that highly. The title will just turn off a significant amount of readers, even thick-skin types whose company monitors web surfing. The new one is better. "We’re going to make an image browser." "Hopefully this example shows that there’s nothing really stopping anyone from using Coq in their Haskell programs today." I hate saying this since the article is well-done but this isn't a demonstration of a verified, image browser in Coq. A verified app is usually considered successful when its extracted code at least runs well enough to be a reference implementation to check others against. The comment in this thread says 6 images kills it on a 16GB RAM machine (?!). It doesn't meet the functional requirement of storing an image collection. It's just an attempt at a verified, image browser that's taken steps toward one that works. Another thing for readers to consider is that making things efficient is a big part of Coq work aimed at real-world applications. The developers usually have to refine the abstract specifications into concrete forms that run efficiently on computers. That takes additional work that looks quite tedious as a non-specialist in formal methods. So, there's two correctness criteria after the thing passes testing (this didn't): it works fast enough to be acceptable in some use case; it works fast enough to be competitive with popular implementations in (insert language). The author might want to build on this example to get it to full correctness with performance at least meeting the first criteria. Then, potentially doing the second to show refinement proof toward efficient, concrete representation. I know Isabelle/HOL is currently really strong in the low-level stuff with some tools synthesizing imperative implementations from functional specs and others verifying assembly. It would be interesting to see what Coq ecosystem can do in automating or reducing effort on similar things. "Using GHCJS on the resulting Haskell to get formally-verified Javascript" Since GHCJS isn't verified, you can't get formally-verified JavaScript by compiling a verified Coq program with it. If anything, you break the verification chain since complex compilers screw things up a lot. Add abstraction mis-matches from cross-compilation to increase chance of a mistake further. I think the accurate statement would just be that using GHCJS would make the program run in a browser or on a JS engine. No longer formally-verified, though.
reificator 9y ago
Look, HN is something that I can justify reading at work, because it's often a great source of both technical articles as well as industry trends. Yesterday I saw this article and the name was exactly what the article was about. I scrolled past and had a laugh, no issues. Today with the short sighted name change it's now an article I would probably click on out of interest, and before you know it I've got a porn tutorial on my screen for the world to see. IMO this article belongs here because it's an interesting approach to an interesting problem. Could the author have chosen a better name/gimmick? Absolutely. But as long as the link reflects the content within, no harm no foul. But changing the name to obfuscate the content within is a reckless choice that I have no respect for. Leave it or delete it, don't make it a gamble to click a link by changing the title.
deleted 9y ago
[deleted]
mcguire 9y ago
* Fixpoint find_categories_ids: Uses "find_category_ids"; this is missing. * newDb version 2 needs a period. * untag_image needs a period. * Theorem preserves_consistency_1: The module MF containing empty_in_iff seems to be defined in the discussion of Theorem preserves_consistency_2. * Require Import Coq.FSets.FMapFacts requires period.
- MichaelBurge 9y ago
  Thanks for reporting these; I've corrected them on the article.

144 points by MichaelBurge 9y ago

sweep4r 9y ago

Writing a porn browser in Coq seems appropriate.

deleted 9y ago
[deleted]
dominotw 9y ago
do americans call their penis cock/dick and vagina pussy when they are having 'sexytime' ? I find saying 'suck my cock' too immature and comical but at the same time 'suck my penis' sounds too clinical and a mood killer.
- andai 9y ago
  ayy bb u wan sum penis?
- wtf_is_up 9y ago
  I prefer to not speak English at all, but to just grunt and make gestures like a chimpanzee.
- deleted 9y ago
  [deleted]

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

lsh 9y ago

+1 - hooray for porn and Haskell

dang 9y ago
Would you please stop posting unsubstantive comments to HN? We're trying for higher quality than that and I'm afraid you've been setting a bad example. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html

logicchains 9y ago

Did you consider using dependent types to define the image database in such a way that it's impossible to create one that's not InternallyConsistent? This approach can often make proofs shorter/simpler.

reuben364 9y ago
Coq isn't very good for developing with properties encoded in the types. Such properties are defined seperately from the data structures involved.

lvkleist 9y ago

this is probably what the creators had in mind when they named the language "coq"

INTPenis 9y ago

Interesting of course but the clickbait title "Porn Browser" made me instantly think of Firefox Focus. I have no idea what build techniques they use but it's definitely a good porn browser in the sense that you can use the family tablet safely and easily with it.

Karrot_Kream 9y ago

Thanks for finally writing an article about Coq that doesn't involve making a compiler. Question: How performant is the generated Haskell code? Also I'd love to see an Idris article next!

MichaelBurge 9y ago
Oh, the performance is the worst. Just initializing the database with 6 images ran my 16GB desktop out of memory. I was able to get it running on a 128GB server I have. The root of it seems to be that something somewhere is using Peano naturals rather than binary ones, and the image timestamps are in the billions. So I worked around it by setting all the timestamps to 1: timestamp <- modificationTimeHiRes <$> getFileStatus filepath return $ DB.MkImage DB.N0 filepath (int_to_n 1) If I banned Peano naturals from all Set-level code and used a better extraction library, I don't see why it couldn't be as fast as Haskell. It might also be worth setting the Strict flag on Haskell for the generated code, since Coq seems designed to target ML, which is strict. Anyone have an idea for an Idris article? Maybe "How to make a Bitcoin exchange or Ethereum contract that's 100% guaranteed not to rob you of your money?"
- iso-8859-1 9y ago
  It's a great idea! Bitcoin needs more formal verification. I wonder how much of e.g. Lightning Network can be proven, assuming SHA256 collisions can't be found, miners include transactions and signatures are unfalsifiable and not malleable. Roasbeef wanted to do it in TLA+, but I am not sure he will find the time.
- sddfd 9y ago
  Why not use a binary number representation? They are in the library: https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNat.htm https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNa... If you use Z, even the Omega tactic (solver for presburger arithmetic) should work.
  - MichaelBurge 9y ago

ImmatureComment 9y ago

Cock browser lol

damnfine 9y ago
You knew these would be downvoted and even made an account name specifically refrencing why. And after all that, a super low effort comment, even for a coq joke. You didn't even try to be humorous or clever... Why bother?
- mcguire 9y ago
  Sometimes, the effort is its own reward.

tempodox 9y ago

So there is a way to formally verify porn? Theresa May might be interested in that.

Simon_says 9y ago
Probably not, since the exact same photo can be classified as porn or not based on the collection of other photos it's grouped with.
KekDemaga 9y ago
”I'll know it when I see it, or when the breast coefficient multiplied by the tumescence index is greater than 9."

nickpsecurity 9y ago

Alright, what I like about this article is it shows the process of specing out the application in a way people new to verification will understand. It's also a useful kind of app instead of a toy language or something. A few critiques follow: " It’s an unspoken truth that most large image databases people have are actually porn collections" Flicker, Tumblr, Imgur, and Facebook Images aren't mostly porn even though one or two are popular for it. So, I doubt that highly. The title will just turn off a significant amount of readers, even thick-skin types whose company monitors web surfing. The new one is better. "We’re going to make an image browser." "Hopefully this example shows that there’s nothing really stopping anyone from using Coq in their Haskell programs today." I hate saying this since the article is well-done but this isn't a demonstration of a verified, image browser in Coq. A verified app is usually considered successful when its extracted code at least runs well enough to be a reference implementation to check others against. The comment in this thread says 6 images kills it on a 16GB RAM machine (?!). It doesn't meet the functional requirement of storing an image collection. It's just an attempt at a verified, image browser that's taken steps toward one that works. Another thing for readers to consider is that making things efficient is a big part of Coq work aimed at real-world applications. The developers usually have to refine the abstract specifications into concrete forms that run efficiently on computers. That takes additional work that looks quite tedious as a non-specialist in formal methods. So, there's two correctness criteria after the thing passes testing (this didn't): it works fast enough to be acceptable in some use case; it works fast enough to be competitive with popular implementations in (insert language). The author might want to build on this example to get it to full correctness with performance at least meeting the first criteria. Then, potentially doing the second to show refinement proof toward efficient, concrete representation. I know Isabelle/HOL is currently really strong in the low-level stuff with some tools synthesizing imperative implementations from functional specs and others verifying assembly. It would be interesting to see what Coq ecosystem can do in automating or reducing effort on similar things. "Using GHCJS on the resulting Haskell to get formally-verified Javascript" Since GHCJS isn't verified, you can't get formally-verified JavaScript by compiling a verified Coq program with it. If anything, you break the verification chain since complex compilers screw things up a lot. Add abstraction mis-matches from cross-compilation to increase chance of a mistake further. I think the accurate statement would just be that using GHCJS would make the program run in a browser or on a JS engine. No longer formally-verified, though.

reificator 9y ago

Look, HN is something that I can justify reading at work, because it's often a great source of both technical articles as well as industry trends. Yesterday I saw this article and the name was exactly what the article was about. I scrolled past and had a laugh, no issues. Today with the short sighted name change it's now an article I would probably click on out of interest, and before you know it I've got a porn tutorial on my screen for the world to see. IMO this article belongs here because it's an interesting approach to an interesting problem. Could the author have chosen a better name/gimmick? Absolutely. But as long as the link reflects the content within, no harm no foul. But changing the name to obfuscate the content within is a reckless choice that I have no respect for. Leave it or delete it, don't make it a gamble to click a link by changing the title.

deleted 9y ago

[deleted]

mcguire 9y ago

* Fixpoint find_categories_ids: Uses "find_category_ids"; this is missing. * newDb version 2 needs a period. * untag_image needs a period. * Theorem preserves_consistency_1: The module MF containing empty_in_iff seems to be defined in the discussion of Theorem preserves_consistency_2. * Require Import Coq.FSets.FMapFacts requires period.

MichaelBurge 9y ago
Thanks for reporting these; I've corrected them on the article.