[pedrocr]

If those languages achieve their memory safety at runtime, like C# does with GC, then that becomes relevant to the point of the compile time performance. The C# compiler has to do less as that complexity has been pushed elsewhere with different tradeoffs.

[pjmlp]

Rust safety with runtime dependencies, Vec bounds checking, Arc and Rc datatypes.

Ada with SPARK 2014 formal proofs, for your other part of the remark.