MISRA C doesn't get me there - it helps, but isn't enough to guarantee the absence of undefined behaviour, despite its 'rule' to avoid UB [0] (which is not mechanically verifiable). It would presumably be possible to use a Turing-complete subset of C, defined such that compliance to it could be verified automatically. I imagine such a subset might be awfully claustrophobic, but my intuition is that this should be possible.
Another approach would be to write code in a different language entirely - either one defined to be free of undefined-behaviour, or one where the absence of it can practically be established statically/automatically. We could then transpile to C code. The transpiler could then guarantee never to generate C code with undefined behaviour.
It seems to be possible to do this today by writing Ada SPARK code and using the (proprietary, terribly pricey) CCG transpiler. [1] (SPARK is a fine choice here. When programming in the SPARK subset, it's impossible to invoke Ada's equivalent of undefined behaviour [0].)
Is there a 'tidier' answer to this problem, or perhaps something obvious that I'm missing?
A related question: is there a 'tidy' way that I can be certain my C code is insensitive to platform-specific behaviours (what C calls unspecified), such as the evaluation-order of argument expressions?
[0] https://learn.adacore.com/courses/SPARK_for_the_MISRA_C_Deve...
[1] https://www.electronicdesign.com/industrial-automation/artic...