[tachyonbeam]

Memory protection isn't just used to protect processes against one another, you can also use it to implement write barriers for a garbage collector, or to map files to memory, for example. I think you'd be hard pressed, with any kind of compiler, to prove that an object you're writing to isn't part of an old GC generation, seems like an intractable problem, unless you're in a pure functional programming language.

[ingenieroariel]

sel4 has a Haskell version that they write before the C (granted, not sure how a ghc generated binary would be verified) but would the problem be tractable in that case?