A Columbo Moment
One of my favourite television shows when I was younger (and still a favourite today when I'm in a reminiscent mood) was Columbo. Peter Falk (one of my favourite character actors) played a natty little police detective who doggedly (and non-violently) pursued murderers with his stock catch-phrase "just one more question".
My Columbo moment came while voraciously reading a book Jeff pointed me to. Written by Richard P. Gabriel, the book is a collection of essays on software development and its community. The "just one more question" popped up as I read this passage:
A small language defined by a group of mathematicians or would-be mathematicians might have a usable formal semantics, and people who wish to prove correctness would be in luck with such a language. But—I hate to be the one to break the news—I’ve been in industry for over 10 years, and I don’t see a whole lot of people proving correctness; I see them reasoning about their programs, but they don’t need a formal semantics to do that.
If you Google on "Haskell prove correct" or some similar phrase, you'll find a lot of people extolling the virtues of Haskell based on how you can make code that is "provably correct". Yet, oddly, I would guess that most of the same people extolling this virtue have themselves never formally proven anything in code beyond some trivial things they did as an exercise.
"Provably correct" code is, I think, a chimera. Whether code is "provable" or not is irrelevant if nobody actually proves it. I think Haskell's virtues are legion without invoking chimeras.
- It's concise.
- It's expressive.
- It permits powerful abstractions to the point of not requiring huge, trivial libraries.
- It supports multi-threaded programming with no change of source code -- the compiler does the work behind the scenes.
- The monadic stuff still blows me away with just how powerful the ability to define whole computational approaches in a libraries. (There's a future blog entry in this if I can ever find the words.)
That's only a short, representative list. I could go on for a long time explaining Haskell's virtues. So why burble on about a capability which is perhaps true, but never used by anybody? Why not focus on things people actually care about?
Posts
2 comments:
Formal verification of Haskell isn't really a chimera, its just expensive.
One of the main Haskell companies, Galois, has its business based on providing formally verified Haskell code. Another interesting project is the verified L4 kernel, which, again, uses formal verification of the Haskell code (via Isabelle), to ensure the kernel API is sound. So, clearly, formal verification matters to some.
To see how expensive it is, have a look at the effect formal verification has on cost and schedule of software. This cost of full verification is why you don't see much of it. Instead, you see lots of semi-formal work, such as using QuickCheck or Catch, to deeply test (or prove, in the case of Catch) particular aspects of program behaviour. The promise of Haskell is thta it will lower the cost of full verification -- not make it as cheap as no verification at all.
OK, "chimera" was perhaps too strong a word. Let's say instead "chimerical to any software 99.9% of developers are likely to ever work on".
I think that, even with Haskell and its lowering of the costs of formal verification, most developers are going to be far more interested in the list I provided (plus the dozen+ other entries I elided from it) than they will be in the "provably correct" angle.
Post a Comment