So, you say they did a KCC-like thing in a theorem prover that could do more than KCC. Then, that it&#x27;s just NIH syndrome against KCC? Seems contradictory. If anything, one would just have to tweak it on a per compiler basis to get it more toward how each implements that behavior. Then it becomes closer to what CompCert did but more flexible.<p>That&#x27;s where I&#x27;d go. Extending KCC to do what a theorem prover could seems more challenging.