I tend to agree. Really the C standard needs to be yeeted away from WG14's grasp. Because they're responsible for blocking safety related improvements.

What do you call seL4, the Compcert C compiler and the tools for writing provably correct C at frama-c.org?

That's called a Chinese Room. :-) A human cannot write correct C. The theorem-prover-human system can. Unfortunately, the C apologists I observe around me are as opposed to formal methods as they are non-C languages. It's some kind of bizarre cowboy thing.

I'd call that a straw man. Very little code is written that way, so it doesn't apply in practice, like... at all.

Also: unless you have very specific requirements there are probably easier languages+tools to write proven-correct programs in.

And we need to stop pretending we do.