Lambda the Ultimate

... why isn't this O'Caml? I was certainly productive with it on my first day of use. Indeed, one of the things that I appreciate about it is that it's deceptively like other functional/imperative/object languages, except that when you want to do genuinely tough stuff, you can, at points where the other languages tend to break down. Jason Hickey at CalTech has written a very nice tutorial for it, and when you're ready for the rabbit hole, there's stuff like Code reuse through polymorphic variants; delimited continuations; monads, complete with do-style notation; dynamically-scoped variables; resumable exceptions; etc. And that's just in O'Caml, without appealing to MetaOCaml, Flow Caml, GCaml...

Those of us who are interested in static type systems are interested in proving properties of our programs before they are released into the wild. We're trying to make those proofs cheaper by making them possible to do by "ordinary compilers." I think it's interesting that there's another move afoot tackling the issues from the other direction, as described here: maybe some of the really good proof assistants with extraction, such as Coq, are already useful to programmers.

Finally, of course, the really exciting stuff is happening around dependent types, abstract interpretation, multi-stage programming, online partial evaluation, etc. where the concepts of "compile-time" and "runtime," let alone "static type" and "dynamic type," get quite blurry. I remain convinced that we can all have our cake and eat it, too, but clearly there's a lot of research and development yet to be done. In the meantime, reasonable people (which I am not) can reasonably disagree as to where to focus their energies. The rest of us can continue to be partisan fanatics. :-)