Hacker News Reader

Comment by IshKebab | Hacker News Reader

> compiler optimizations are just extremely prone to mistakes

This is definitely true - there has been quite a lot of formal work done to prove that optimisation passes don't change semantics. I guess it hasn't made it into Rust yet. Or maybe even LLVM.

View on HN

Formal proofs for specific instruction sequence substitution (e.g. LLVM's instcombine) are simple-ish enough via just throwing SMT at it, ...as long as the source pattern and target replacement are in a format from which both the compiler code and verification source+target can be automatically derived from; though you'd still need manual proofs for anything with unbounded configurations that can't be exhaustively checked if you aren't satisfied with just checking some subset.

Larger-scale things operating over an unbounded amount of instructions require significant amounts of effort of verification on each pass. CompCert apparently has 1200LoC of proving DCE, one of the simplest whole-function passes - https://github.com/AbsInt/CompCert/blob/02fc017cf69210db5fd5...

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.

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.

Reply on news.ycombinator.com