5 ms·

A functionally correct and slow compiler is not very useful and is almost certainly a waste of effort to implement.

• steveklabnik 4y ago
  Especially because the whole point is to qualify the compiler. You can't say "well this code compiles under the reference compiler but in production we compile it with this other compiler," as that's like, kinda the whole point of qualification: to qualify the tools being actually used.
  • OJFord 4y ago
    You could produce final binaries for QA & shipping with the qualified one, and develop with something faster? Sort of analogous to 'optimisations' and debug symbols.
    • steveklabnik 4y ago
      Sure, but given that the qualified one here still needs to be good enough to produce production ready code, you're not really saving yourself any work. especially given that many use cases for this sort of thing are either embedded or close enough, and that Rust really relies on optimizations to produce good code, you need more than a bare minimum "it works" compiler to make the whole thing go. My team's embedded project sets opt-level 1 even in debug builds, as no optimizations makes things impossible, flash size wise, and we're not even working with particularly small MCUs.
  • typesanitizer 4y ago
    I don't think this is entirely accurate. For example, the Translation Validation section on this Wikipedia page mentions (https://en.wikipedia.org/wiki/Compiler_correctness https://en.wikipedia.org/wiki/Compiler_correctness) > Translation validation can be used even with a compiler that sometimes generates incorrect code, as long as this incorrect does not manifest itself for a given program. Depending on the input program the translation validation can fail (because the generated code is wrong or the translation validation technique is too weak to show correctness). However, if translation validation succeeds, then the compiled program is guaranteed to be correct for all inputs. I don't remember where I read this, but I think there are some examples in practice where instead of proving the correctness of some optimizations of existing C compilers (which is a codebase that keeps evolving), there have been situations where the correctness was ensured using program equivalence checking. So you'd "freeze" the reference compiler and the equivalence checker (which would be qualified), and pair that with an upstream compiler with sophisticated optimizations. So long as the equivalence checker keeps passing, you're golden.
    • steveklabnik 4y ago
      I guess to me I see that as isomorphic; you're still qualifying the output, even if there's an intermediate step involved. The path towards qualifying the output of the sophisticated compiler may be more indirect, but you're still doing it.
    • denotational 4y ago
      > I don't remember where I read this, but I think there are some examples in practice where instead of proving the correctness of some optimizations of existing C compilers (which is a codebase that keeps evolving), there have been situations where the correctness was ensured using program equivalence checking. This is what CompCert does (or at least did when I last looked inside CompCert) for register allocation; the graph colouring algorithm is unverified, but a verified validator is used to check the colouring is correct. Whilst this is relatively straightforward for something like graph colouring, it is substantially more difficult for comparing the outputs of two different compilers, which I think is what you are suggesting here? There was some work to do a translation validation for the entire RTL -> LTL pass of CompCert, but I'm not sure how much progress was made or if this is currently used.
• dwohnitmok 4y ago
  Depends on the details of how you're formalizing your verification and what tools you have at your disposal. It could be immensely useful as a stand-in for a specification since it reduces a large class of verification to "does it do the same thing as the reference compiler." E.g. it's a huge amount of work to exhaustively formally specify the Rust type system (as opposed to just specify it in English). However, if you already have an assumed correct, but slow, type checker then your verification effort can boil down to just "does my compiler have a type error if [and only if if you care about more than just safety properties] the reference compiler has a type error?" That's still an enormous amount of work to verify, but is comparatively trivial to specify.