Comment by hinkley

We are going the long way around to figure out that Tannenbaum was right and we need microkernels. The IPC costs cause sticker shock, but at the end of the day perhaps they are table stakes for a provably correct system.