This will not be a security paradise, because there's plenty of other ways to screw up. Even if we magick a perfect capabilities-based system into existence in 2040, with every desirable property that is promised fully manifested, programmers will still fail to correctly use it, because security is profoundly a Hard Problem. But the same freaking buffer exploit for the ten millionth time should be a thing of the past. (Library support should also be well on its way to making cross-site scripting a thing of the past, too.)
There is a version of the L4 microkernel that has been formally verified which should prevent memory corruption in kernel space, but I don't know the exact details.
This of course won't prevent corruption due to physical sources, such as radiation, but with physical access to a machine you will always be able to gain access.
The second thing is that while a microkernel (if used with an IOMMU to prevent a malicious driver from DMAing all over your code) appealingly prevents an attacker from exploiting a malloc overflow in some random network driver and immediately gaining full access to anything (the current state of kernel security!-- but performance is key), it doesn't prevent an attacker from using that network driver pwn to hijack the user's Facebook session; full access is appealing, but in a complex system there are many, many "lesser targets" that are just as bad from a user's point of view.
Microkernels and their little cousin sandboxing can help, but the resulting trusted computing base is still much, much larger than we can formally verify in the foreseeable future.
(A sibling of this comment mentioned Singularity, but that's a fairly different beast: instead of proving that fast code is safe, you try to make obviously (memory) safe code fast. The only reason Singularity is able to make interesting performance claims is that it uses verification to completely avoid system calls: pretty cool, but a NaCl-like kernel could do something fairly similar for C; it doesn't really change the correctness/performance tradeoff.)
I guess it's turtles all the way down. http://en.wikipedia.org/wiki/Turtles_all_the_way_down
But complicated type systems are, unfortunately, rarely used in languages suitable for system programming. I only know about ATS in this group actually :-)
I have some hope for Rust because their type invariants system (I forget what they're calling it) lets you glue some of this information to variables in a compelling way without necessarily having to solve all the theoretical and practical problems that come with full dependent typing.
We'll see, I guess.
int array[10];
Plan9 ain't bad either. There's also different C# clones (that aren't based on Singularity)
http://sip.cs.princeton.edu/pub/memerr.pdf
Neat hack :)