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.