[yeputons]

>How is it possible that I can write efficient and provably-safe code in C# without a degree in type theory?

Because of two things mentioned in the article just below.

> Here we see C#’s first trade-off: lifetimes are less explicit, but also less powerful.

If C# is less powerful, it does not need powerful syntax. One does not need explicit lifetimes in Rust for a long time either, deduction work just fine.

> The escape hatch: garbage collection

If C# is ok with not tracking _all_ lifetimes _exactly_, it does not need powerful syntax. Not an option in Rust, by design.

Basically, not all code is possible to write, and not all code is as efficient.

[daxfohl]

Both have "unsafe" escape hatches, so all code is possible to write efficiently. Just some cases are harder to prove correct in the type systems of each.