Objection was against "memory safety" somehow having become "safety". Here is an epic tool that allows one to attach and formally prove assertions. Genuinely impressive and massively useful.

Yet the pitch is that it is needed for the "unsafe" unsafe code, to make it "safe". Not for all code, to make all code safe.