The whole problem is that you only need one mistake in all those billions/trillions of LOC's, and your systems get 0wned. I'm pretty sure that "our standards for C programmers" don't include "programmer is guaranteed not to make any mistake, EVAR", whereas that's an entirely appropriate standard for automated, language-based security.