1. 9

  2. 3

    [Reposting article and comment from HN. Note they changed title to “image browser” which is smarter. Just edited the title as it’s already getting downvotes or Coq jokes.]

    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.

    1. -1

      I’m not familiar with Coq but I find the name in conjunction with “porn browser” strangely appropriate.

      1. 4

        I’m not sure what all this has to do with birds?