5 ms·

It is true that there might be errors in anything. However, this is mitigated by having only a very small core that checks the proofs. Basically if there if a

by scscsc 12y ago

It is true that there might be errors in anything. However, this is mitigated by having only a very small core that checks the proofs. Basically if there if a wrong proof goes through, there must be an error in the core (which was checked by many people and is very small).

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 ago
  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.
Drakim 12y ago
I agree that the chances are pretty small, but is that "good enough" when it comes to formally verifying things? (I know next to nothing about formal verification)
- scscsc 12y ago
  Well, that's also true. But apparently there is no better thing to do. There is always a disconnect between what you mean and what you say. It happens all the time and the risk is not going to go away. People who work with proof assistants understand this risk better and most of them are pretty happy that the risk is sufficiently small for their purposes.

by scscsc 12y ago

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 ago
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.

Drakim 12y ago

I agree that the chances are pretty small, but is that "good enough" when it comes to formally verifying things? (I know next to nothing about formal verification)

scscsc 12y ago
Well, that's also true. But apparently there is no better thing to do. There is always a disconnect between what you mean and what you say. It happens all the time and the risk is not going to go away. People who work with proof assistants understand this risk better and most of them are pretty happy that the risk is sufficiently small for their purposes.