| A problem to consider: Arbitrarily complex programs makes even defining what is and isnt a bug arbitrarily complex Did you want the computer to switch off at random button press; did you want two processes to swap half their memory. Maybe, maybe not A second problem to consider is that verification is arbitrarily harder than simply running a program -- often to the extent of being impossible, even for sensible and useful functionality. This is why programs that get verified either don't allocate or do bounded allocations. But unbounded allocation is useful It is possible to push proven or sanboxed parts across the kernel boundary. Maybe we should increase those opportunities? Also separate address spaces simplify separate threads -- since they do not need to keep updating a single shared address space. So L1 and L2 cache should definitely give address separation. Page tables is one way to maintain that illusion for the shared resource of main memory... Probably a good thing That's not to say there isn't a lot of space to explore your idea. It is probably an idea worth following One final thought: verification is complex because computers are complex. Simplifying how processes interact at the hardware level. Shifts the burden of verification from arbitrarily long running and arbitrarily complex and changing software; to verifying fixed and predefined limitations on functionality. That second one has got to be the easier to verify |