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?
"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?
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.
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.
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
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.
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.
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.
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)
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."
[1] https://www.microsoft.com/en-us/research/project/pex-and-mol...
[2] http://blog.thecodewhisperer.com/permalink/integrated-tests-...
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.