someone's gotta write the kernels though, I can't think of any way to write kernels or compilers where memory corruption is impossible.
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.)
But given that 2040 was the year tossed in, I was also thinking the next generation after that, where some of the next-next generation of verification would be folded in. There you're looking at Haskell as being the gateway into that world (even though it is not really that verifiable in the strongest sense itself, it gets your foot in the door), and the Coq and Agda and the slowly-but-surely increasingly usable proof assistants, which would be useful for a provable-not-corruptable (via normal software means) software kernel.
Though... if one looks at the rate of advance in kernels over the past 30 years and then project out to the next 30, we get a distressingly high probability of it still being in C. Still, I cautiously optimistically (or pessimistically, depending) think that the hardware revolution that we are still only at the beginning of as we run out of Moore's Law is going to produce non-C languages that will eventually be irresistible to produce kernels in. There's going to be ever more constraints we want to maintain and it's going to get harder and harder to maintain them without some sort of language support beyond what C can supply.
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.
I guess it's turtles all the way down. http://en.wikipedia.org/wiki/Turtles_all_the_way_down
So it's not useless.
The higher level question is whether the Haskell specification fully and correctly specifies the desired behavior. In my 30-odd years of experience in Mil/Aerospace, I have never seen a fully and correctly specified set of requirements that could be transliterated into correct executable code. If nothing else, they all have had implicit assumptions. That is the Achilles heel of the IBM "Master Programmer" method, reborn as "outsourcing".
Since the specification is executable Haskell, that implies they wrote Haskell test programs to show that the specification implements the desired behavior.
Writing a program to verify the specification that another program implements... and then claiming a formal proof of correctness of the system is now recursive. Turtles all the way down.
For others: I learned a lot from reading the book "Mechanizing Proof". No knowledge of formal methods is needed (but you will learn something about formal methods while reading). I can't recommend the book highly enough.
http://www.amazon.com/Mechanizing-Proof-Computing-Inside-Tec...
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.)
That is a very far cry from saying we can live in a world with perfect security, which I think is the point you are trying to make.
While none of this is bullet proof, it does add a very customizable kernel-level "sandbox". If you can't run your exploit for example, even thus the kernel is vulnerable, well, too bad.
Now for dreaming out loud, let's go code an OS in Rust that mimics most of Singularity and adds some RBAC on top for good measure (even thus its a much lighter version than on traditional OSes due to the system call avoidance and inherent sandboxing of all apps, as well as the contracted messages.)
But complicated type systems are, unfortunately, rarely used in languages suitable for system programming. I only know about ATS in this group actually :-)
int array[10];
With dependent types function to get element from array may have type (this is pseudocode): get (array : T[n], index : m) : T {n : nat, m : nat, m < n} which would mean "function get, which takes: n long array of elements of type T, index of type m, where m is smaller than n, and returns T". Type-level naturals and bounded array access are the basic examples of dependent typing, more interesting ones may be red-black trees with guarantees about their shape put in the type or some magic for creating DSLs.
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.
Plan9 ain't bad either. There's also different C# clones (that aren't based on Singularity)