4 ms·

The C spec and x86 assembly are two very well known specs.

• vertex-four 12y ago
  If they're very well known and everyone can understand them and implement them perfectly, we wouldn't need formal verification in the first place. I don't doubt that formal verification significantly reduces the chances of bugs, but it's not a panacea, or we have computers that read our minds. You still need to verify that the proof is proving the right thing, although you can be sure that it's internally consistent.
  • more_original 12y ago
    > If they're very well known and everyone can understand them and implement them perfectly, we wouldn't need formal verification in the first place. We're verifying the compiler from one language to the other. The specifications of the two languages are not that hard to implement. The difficulty is covering all cases in compiling from one to the other. The formal proof does tell us that we haven't missed any.