3 ms·
You have to translate between the English spec and the computer-readable proof, and surely it's relatively easy to mess that up in some way and end up proving t
by vertex-four 12y ago
You have to translate between the English spec and the computer-readable proof, and surely it's relatively easy to mess that up in some way and end up proving the wrong thing.
- qznc 12y agoThe C spec and x86 assembly are two very well known specs.
- vertex-four 12y agoIf 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.