The idea of having a small kernel that is properly verified, and properly run user-level code in a memory-protected manner isn't absurd. And when put into the context of Operating System budgets, 4.6 Million dollars is completely reasonable. Again, we're also talking about a hypothetical 2040 OS. not something we're going to have working tomorrow.
I didn't mean to imply it's not possible, or won't be possible in the future, just that I don't think it's on the immediate horizon for anything but small kernels. 4.6 million dollars may be reasonable, but if you have to add on another million dollars and another month of verification time for every patch release... it's just not practical yet.
