That's true. The immediate-term impact is probably minimal, for the reasons you mention. However, this is a major accomplishment. As this work is built upon, its longer-term impact has the potential to be very significant.
I agree it is a major accomplishment. I have doubts about its impact, because I am unsure whether it will be built upon.
CH2O's main innovation is C standard (as opposed to C implementation) formalized in general purpose prover (as opposed to custom system). KCC formalized C standard, but not in general purpose prover. CompCert formalized in general purpose prover, but formalized implementation instead of standard.
Formalizing in general purpose prover is useful because you can use all of math to prove runtime invariants. But if you want to prove runtime invariants, you usually want to prove with respect to concrete implementation, not to prove abstractly to standard. For time when you want to prove abstractly to standard, this doesn't seem better than KCC.
In short, this feels like Not Invented Here against KCC. Probably unfair characterization, but that's what it feels to me.
So, you say they did a KCC-like thing in a theorem prover that could do more than KCC. Then, that it'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.
That's where I'd go. Extending KCC to do what a theorem prover could seems more challenging.
That seems to be what he says, but after the first part he disregards that as not useful. Another comment points out following the standard is good for portabilities sake. Somehow, that all seems obvious to me.
That was the build up. It led to the following statement and conclusion:
"For time when you want to prove abstractly to standard, this doesn't seem better than KCC. In short, this feels like Not Invented Here against KCC. Probably unfair characterization, but that's what it feels to me."
The obvious interpretation is commenter thinking KCC is better and (see NIH) the OP should've maybe done something with it instead...?
" Another comment points out following the standard is good for portabilities sake. Somehow, that all seems obvious to me."
You can follow the standard and be portable if you keep certain parts as options subject to interpretation/choice of the implementers. That's the so-called undefined behavior mostly.
> But if you want to prove runtime invariants, you usually want to prove with respect to concrete implementation, not to prove abstractly to standard.
Really? I would think that if you're trying to write a portable program, it would be much more useful to prove invariants based on the language specification, not a particular concrete implementation.
