> There's a formal proof asserting that if you keep up the safety invariants within an unsafe region then that will not infect other code, even in the presence of arbitrary other correctly-written unsafe blocks.
In general "unsafe" does not compose.
"if you keep up the safety invariants within an unsafe region"
In general "unsafe" does not compose.
"if you keep up the safety invariants within an unsafe region"
This condition is doing a lot of heavy lifting.