[emorning4]

I can't imagine how writing C directly could possibly be better than using a language like Dafny and then generating C code.

Edit: Dafny: A verification language capable of enforcing invariants

[emorning4]

Down-voting me without providing a counter comment is just pathetic.