For C and C++, the cost of proving a compiler correct seems hugely out of proportion to the actual benefit gained from doing so. Most critical security bugs in C++ code are found in code that the compiler had no obligations whatsoever to compile "properly", because they are the result of undefined behavior (use after free, buffer overflows, stray writes, etc.) A perfect, proven-correct C++ compiler would do nothing to protect against any of the famous vulnerabilities you've heard of. Even the famous "null check eliminated by a GCC optimization" Linux kernel bug would be unaffected, as that was a valid optimization per the language definition.

By contrast, I think JavaScript VMs are the target of miscompilation attacks many of orders of magnitude more often than C++ compilers are. They actually have to compile untrusted and hostile code. A miscompilation can be disastrous, and in fact actual browser vulnerabilities have traced back to incorrect JS compilation. So I feel this impressive research might have a more practical impact if applied to JS (or Web Assembly!)

The KCC compiler will crash/stall on a program if it detects undefined behavior. Those willing to accept the penalty or separately verify those structures needing it can still benefit. If they need the performance & won't just do assembly, then they won't use such a tool as you said. That's why formal, equivalence checks for optimizing compilers are important. Need that work finished fast since it might help here.

wbl

Undefined behavior isn't something that can be detected. Any addition of signed integers might be undefined behavior. What UB means is the compiler can apply transformations only correct in the range where UB doesn't happen.

wuch

I presume that KCC in question is https://github.com/kframework/c-semantics, i.e., a formalization of C programming language in a form suitable for evaluation. It indeed can detect undefined behaviour, though last time I played with it (a few years ago) it was hardly something that you can use on anything but trivial examples. Not to mention that it crashed on various implementation defined behaviours (for example comparing unrelated pointers with <) limiting its usefulness even further.

BTW, both gcc and clang contain runtime checker for easily detectable undefined behaviours like singed overflow you have mentioned. You can enable it with -fsanitize=undefined.