3 ms·

Here's a dumbed down explanation. This actually isn't systems programming, this is compiler technology. It is an effort to prove that the LLVM compiler framewo

by exDM69 12y ago

Here's a dumbed down explanation. This actually isn't systems programming, this is compiler technology. It is an effort to prove that the LLVM compiler framework (or at least parts of it) work correctly. Proving here means formal verification, not too dissimilar from making a mathematical proof that something holds. Basically the idea is to look at the optimizations that the LLVM compiler performs and verify that the program after the optimization does the same thing as before optimization. It is easy to write compilers that emit fast code, but a lot harder to write compilers that emit fast and correct code.

dspillett 12y ago
> but a lot harder to write compilers that emit fast and correct code. The hard part is being confident you have correct code for all cases even the rare edge cases. Producing something that works for the happy path is easy. Producing something that works correctly for a wide range of input test conditions is more long winded but still not difficult. This sort of work is about mapping the inputs, assumptions, and outputs into a minimal (mathematical) form and using that to prove that for all cases the process correctly maps one to the other - to try prove that there can be no input for which the output is invalid.