The C89/C90 wording change story is a myth. And I am not sure I understand your point about CompCert. The correctness proof of CompCert covers programs that have no UB. And programmers do have some choice and also some voice. But I do not see them pushing for changes a lot.
The choice is going for other languages because they don't believe WG14, or WG21 will ever sort this out, as many are doing nowadays.
This is my point, programmers apparently fail to understand that they would need to push for changes at the compiler level. The committee is supposed to standardize what exist, it has no real power to change anything against the will of the compiler vendors.