[uecker]

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.

[ummonk]

The C standard changed its note about "permissible" undefined behavior (in C89/90) to "possible" undefined behavior (from C99 onwards). This is easily verifiable and not a myth.

As to CompCert, I'm not sure if they still make guarantees about type punning, but the older paper had said this:

"The semantics of Clight is formally defined in big-step operational style. The semantics is deterministic and makes precise a number of behaviors left unspecified or undefined in the ISO C standard, such as the sizes of data types, the results of signed arithmetic operations in case of overflow, and the evaluation order. Other undefined C behaviors are consistently turned into “going wrong” behaviors, such as dereferencing the null pointer or accessing arrays out of bounds. Memory is modeled as a collection of disjoint blocks, each block being accessed through byte offsets; pointer values are pairs of a block identifier and a byte offset. This way, pointer arithmetic is modeled accurately, even in the presence of casts between incompatible pointer types"

[pjmlp]

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.

[uecker]

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.