While presenting the Pragmatic Real-World Scala talk at QCon London 2009, Jonas Bonér introduced functional programming as something that ultimately leads to more usable code and compared it to Lego, in a sense that you can take functions, combine them easily to get new functions etc. Sounds familiar? OO anyone? Stop the Lego analogies, please.
I remember exactly the same marketing messages for object oriented software, where lego-like boxes will be magically combined with other lego-like boxes to produce other boxes and everything will be nice and green and pink bunnies will jump all around us..
I appreciate that functional programming is a different paradigm where statelessness can help a lot with parallel processing, and the revival of the interest in that is probably the only useful thing that came out of computer science academic projects in the last decade, but are the real benefits of it usable code and lego-like combinatorial promise that often ends up as a mess? Please tell me that there is more to functional programming than that.
Bonér sort of lost me at a point where he said that unlike objects, functions can be mathematically proven that they are correct. Some of the most respected scientific minds in the computer science history disagree with this. Donald Knuth’s famous quote on this is “Beware of bugs in the above code. I have only proven it correct, not tested it.” C.A.R. Hoare said this morning that “You cannot ask a scientist to check whether a program does not contain undesirable features.”. How can you mathematically prove that something doesn’t have bugs? I’d really like this promise to deliver but it seems completely unrealistic.
Too bad – the start of the presentation introducing Scala was really interesting and I looked forward to learning something new.
I will be covering QCon 09 in detail on this blog. Click here for other news and reviews from the conference.
|
|
“it is probably the only useful thing that came out of computer science academic projects in the last decade”
Functional programming predates Object Oriented programming (if anything they were discovered concurrently). It is not new. It is just new to you.
Also… burn! What a rude thing to say.
The proposition of being able to verify program correcteness is something that keeps appearing from time to time. I don’t understand why people do not take two seconds to think and reach the right conclusion.
Repeat with me: IT IS NOT POSSIBLE. Period. Want a proof? Of course, a year long course on logic would mathematically prove it. But there is a another argument that is much shorter, does not require three years of preparatory study and is understood by anyone who sits down and thinks twice about it.
The argument is so simple that it does not even require a blog post to explain. Still with me? Ok, here we go. It’s not possible to have something that proves that a program is correct. Because that “something” would need to be proven correct, and whatever you devise to prove that correct would also need to be proven correct as well, which means that you build a proof that needs to be proven that in turn…. repeat ad infinitum.
Of course, that does not mean that there are ways to ensure that your program is more likely to be right. And probably functional programming is one of them. But the more you get close to functional programming and formal verification, the more you distance yourself from the problem domain. And thus, you lose in the way to correctness a lot of people that simply don’t feel like being productive defining assertions and pre and post conditions.
Oh, and about the Lego analogy, could you please devote another post to that timely classic “the end of programming”?
Hmmm. I’ve got a port of an (almost) functional language called pbLua running on my LEGO MINDSTORMS NXT. But that’s not what I’m commenting on
The LEGO analogy of software reuse is indeed shopworn and does not stand up to scrutiny. Perhaps managers like the fact that reusable software is supposed to be like building blocks, and LEGO is like building blocks, therefore ….
In fact, a typical software project is like dumping a tub of random parts onto a table and being asked to design a specific thing with those parts. Oh, and while you’re building it, the marketing guys will ask you to make all of it one colour (or at least use pretty ones that go together) and to make sure that it holds together when a 4 year old plays with it.
Here’s another quote from Knuth:
They haven’t yet built a reliable way to reason about these programs, that is, we still lack the mathematical proofs to ensure a program will work. With object oriented programs, we have much less of an understanding of how we would ever prove that they don’t have bugs. This is a huge gap. If people can understand OOP, they ought to be able to prove that the programs are correct.
(Read the whole interview at http://www.literateprogramming.com/byte1996.html)