Thank you so much for the answer!
I guess I was wondering why a new C project wouldn’t consider CompCert…the hope of porting seems basically 0, but I was wondering why it wouldn’t be in the running for new projects.
I asked a friend who writes a lot of C professionally and he said a lot of the missing language features would already be show stoppers, but more generally was suspicious of the value, which I thought was a shame (basically, he felt that dynamic analysis would get more of the reward without having to switch to an inferior tool chain and engage in a bunch of very difficult proofs).
The point about gcc and clang being about software development and not just compilation is also a good one. But they’re all good points
At some point I want to try to do something smallish but non-trivial in verified C and see how much of a bear it is…
Edit: I guess there are also some contexts where the costs of failure are very, very high. While I would never want to support military applications, an F35 for example which costs like a billion dollars. Or space probes. Perhaps in practice the things which sink this could not be helped by compcert (and something like verified C). I know that they have extremely laborious code review and testing standards, though.