Developers use unsafe programming languages for low-level systems code due to performance concerns. Unsafety causes bugs and security vulnerabilities that safe languages eliminate. We argue that languages can provide safety without run-time overhead by exposing types with the invariants needed to prove the safety of operations. We empirically show that Rust and C# can be extended with such features to implement safe network drivers without run-time overhead, and that Ada has the necessary features already.