Oh yes, it is still a better situation. Although C compilers are quite buggy.

Since Lean can emit LLVM it might be more achievable to reach performant assembly without going via C. All sorts of interesting work in progress.

https://dl.acm.org/doi/10.1145/3192366.3192377

(I am rate limited to ~5 comments a day so not replying for ages is just a function of the HN gods on Mt Sunnyvale.)