[rtpg]

Not to minimise compcert's work nor to trivialise the equivalent kind of work in Rust but I wonder how much of the Compcert difficulty on dead code elimination is downstream of C semantic futziness. I know that CompCert has a whole notion of external visibility that it has to deal with that I _think_ would be way more straightforward in Rust.

My experience writing Roq (very limited!!!) is that it also lends towards kinda brute forcing your way through something. If you have your set of proof lemmas and you tie it all together there's not that much incentive to simplify the proofs (that are irrelevant anyways, according to the theories). So the 1200 LoC might be "oh we could have maybe done this in 400 with more thinking but ... well... this is working yeah?"

trying not to trivialize it all. Just kinda hoping that we do have a more provable future ahead of us, and that CompCert represents (hopefully) an upper bound of difficulty just due to the nature of the source language.

[dzaima]

Perhaps some early things in the pipeline could be easier with a saner language, but I can't imagine it affecting much of the core optimizations, which'd all benefit from being ran on some messy low-level intermediate form equivalent to what C converts to anyway (if not more complex if preserving precise aliasing info). Would be curious to hear about that external visibility thing, doesn't feel like it could make optimizations (beyond inlining, perhaps?) harder.