This sounds very impressive, but if you think about it they've really solved a very uninteresting problem. What they have done is essentially layered a sound type system on top of C, and run a particular C program (the kernel) through this type checker. (It's a little more sophisticated than that, but that's the gist of it.) You could accomplish exactly the same thing by simply writing the code in a language like Haskell or Lisp that had a sound type system built in as part of its design. Haskell and Lisp programs have all the same properties as the L4 kernel: they never overflow their buffers, never dereference null pointers, never leak memory, and never have arithmetic overflows. But when you think about it that way, it's a much less impressive result. The only thing that makes this interesting at all is that they wrote their code in C. This is rather like climbing a mountain carrying a 500lb weight. Yes, in a sense it's impressive, but it's a lot easier to scale the mountain if you just don't pick up that 500lb weight to begin with.
Yes, I know. I don't want to diminish their accomplishment. They did in fact scale the mountain. My point is only that they made it harder on themselves than they had to by choosing to focus their efforts on a C program. They could have accomplished exactly the same thing with a lot less effort by simply writing their code in Haskell (or Lisp or Qi) to begin with. But then the headline would have been "We wrote an OS kernel in Haskell" which would not have sounded nearly as impressive.
