Both House OS in Haskell and SVA-OS handled that by cleanly hiding unsafe details behind an interface that could be used safely: http://programatica.cs.pdx.edu

Both House OS in Haskell and SVA-OS handled that by cleanly hiding unsafe details behind an interface that could be used safely: http://programatica.cs.pdx.edu/House/ http://programatica.cs.pdx.edu/House/ https://llvm.org/pubs/2009-08-12-UsenixSecurity-SafeSVAOS.html https://llvm.org/pubs/2009-08-12-UsenixSecurity-SafeSVAOS.ht... So, that's not really a limitation. Worst-case scenario is proving those primitives correct with external tools whose preconditions and invariants are just checked by memory-safe code calling it. The above work shows worst case might not happen, though.