<i>&quot;Maybe when we make more progress with formal proof-generating languages, we can create a &quot;friendly&quot; C where the compiler refuses to compile the code until it&#x27;s accompanied by formal proofs of UB-avoidance.&quot;</i><p>That&#x27;s entirely feasible.  I headed a team which did that for a dialect of Pascal over three decades ago.[1]  It&#x27;s since been done for Modula III, Java, Spec#, and Microsoft Windows drivers.<p>One reasonable thing to do is to have the compiler generate run-time assertions for every statement which has a precondition for defined behavior. All pointer dereferences get &quot;assert(p != 0)&quot;.  The shift problem in the original article gets &quot;assert(n &gt; 0); assert(n &lt;= 32);&quot;  Now everything has run-time checks.<p>Then you try to optimize out the run-time checks, or at least hoist them out of loops. A simple prover can remove about 90% of the checks without much effort.<p>[1] <a href="http:&#x2F;&#x2F;www.animats.com&#x2F;papers&#x2F;verifier&#x2F;verifiermanual.pdf" rel="nofollow">http:&#x2F;&#x2F;www.animats.com&#x2F;papers&#x2F;verifier&#x2F;verifiermanual.pdf</a>