[theta_d]

It does have GC but that is not the point being made.

I believe the point the author is making is that other languages provide better safety than C and have faster compile times than Rust, therefore Rust should be able to improve its compile times.

[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.

[rbanffy]

GC is not a roadblock for OS kernel work. Smalltalk is itself an OS and had GC from the start. IBM's i (the descendant of OS/400) most likely has GC as part of its kernel. Lisp machines had hardware-assisted GC.

What you may want to try to avoid is complex and non-deterministic GC, which makes it harder to reason about.