Something very cool about this GC is that it's written in F* (technically, a low-level subset called Low<i>) and compiles to </i>memory-safe C,* so it's kind of equivalent to using Rust but they don't have to give up C.<p>F<i>/Low</i> are also used in Project Everest, which ships formally verified crypto primitives in Firefox and other platforms.