3 ms·
Great question. They don't have to trust the compiler: after compilation, they use an SMT-based proof process to establish that the resulting binary matches the
by saithound 7y ago
Great question. They don't have to trust the compiler: after compilation, they use an SMT-based proof process to establish that the resulting binary matches the semantics of the C source directly. See https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf https://ts.data61.csiro.au/publications/nicta_full_text/6449....
- zingermc 7y agoAh, it appears that is only done for ARM, but not x86. It would be great if x86 were more amenable to FM, or if we had faster formally-specified processors. Can't wait for a RISC-V workstation!