Scopes does not segregate unsafe and safe code, and consequently does not provide any way of proving whether a particular function invokes unsafe code. A new keyword unsafe must be added, which defines a region of code that allows unsafe operations, and then the prover must be augmented to tag every single potentially unsafe operation. If these operations occur outside an unsafe context, a compiler error should be generated.
Scopes does not segregate unsafe and safe code, and consequently does not provide any way of proving whether a particular function invokes unsafe code. A new keyword
unsafemust be added, which defines a region of code that allows unsafe operations, and then the prover must be augmented to tag every single potentially unsafe operation. If these operations occur outside an unsafe context, a compiler error should be generated.