Arguably C doesn't: C is just what the spec says. You can try and formalise what the spec says (as, rightly, many have done), but it's hard to guarantee correct

Arguably C doesn't: C is just what the spec says. You can try and formalise what the spec says (as, rightly, many have done), but it's hard to guarantee correctness of that formalisation.