On Fri, Jul 31, 2020 at 3:55 PM Jon P <[email protected]> wrote:
> > Hi Mario, > > Very nice talk, thank you for posting it. > > Is it ok to ask some basic questions? It is a really nice project you are > doing and I would love to understand it, however I am afraid I am not so > strong in all this stuff. Feel free not to answer if you are busy, that is > no problem, if it's ok I'll just write what I think and then maybe you > could tell me where I have got confused? > > So I understand about metamath. You have some hypotheses and a theorem and > a list of substitutions which use rules from the database or hypotheses to > establish the theorem. I also understand that there is a question around > whether you can trust the verifier, so we have 5 independent ones to > improve that. > > I think I also get a little of the idea of formal verification for > programs, so you have some abstract model of a computation system (like > x86) and using that you prove that, if the hardware executes the model > accurately, that the program will give the output you want. Like maybe some > function called Prime(X) which returns 0 for primes and 1 for non-primes, > you could prove that, if this terminates, the answer will be correct. > However I guess there is still the problem of trusting the verifier > (whether human or machine). I also have never seen a verification of a > program so if you know any beginner materials on it I'd be interested. > > I think you're trying to combine both of these right? From what I > understand of your system there's MM0, which is a verifier, which takes and > mm0 and mmb files and checks if the proof is correct. I assume this is much > like the metamath verifiers? Then there is MM1 which is a tool for > generating mm0 and mmb files which is not verified but it doesn't matter > because it's output is checked so how the output was generated is not > important. > > And then there is MMC which is a language which compiles programs and also > creates proofs of the correctness of those programs? So if I write some > program, like Prime(X), the compiler will output some machine code and also > a proof that Prime(X) does what it is specified to do, on x86, up to the > assumption that the hardware executes the model correctly? And the idea is > to write the MM0 verifier in MMC so that it is verified during the > compilation process which gives confidence in it? > That's correct. You said that we ensure the correctness of the metamath verifiers by having many of them, I want to go one step further and verify that the program itself is implemented correctly with a formal proof. If that is all reasonably correct I guess where I am confused is how you > are doing this reflexive verification. > > I would have thought, naively, that for justifying any program, X, you > have 3 options. Firstly you can assume X is valid. Secondly you can use Y > to justify X, the problem of this is that it's then justifications all the > way down. Thirdly you can use X to justify X, as in if the program is a > program verifier then you can feed it into itself and if it says it's good > then it's good. > > However I don't understand how that's not circular? For example consider > the verifier: For all input return "this program is verified." That has the > ability to verify itself and will come out with a positive response however > I don't think it's really established anything particularly meaningful. I > guess I can't see on a philosophical level how you can get out of that trap. > It is circular, I don't contest it. I go into more detail on the philosophical implications of self-verification in a previous talk I gave in January on the topic: http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_carneiro.pdf https://www.youtube.com/watch?v=CqZzbaEuNBs The point is that even a circular proof of correctness is an improvement on no proof of correctness, it's just not as good as a non-circular proof. In order to make up the difference you still have to look at the code and verify that it's reasonable. You have to do this with a standard unverified kernel too, only now you have the assurance that the fine details are correct and the inspection is to make sure that there aren't any obvious problems. The need for inspection also means that it is important for the bootstrap to be as small as possible. It should also be possible to set even smaller programs under MM0, but these will not be self verifying, they rely on full inspection (or rather, they can be verified by MM0, not themselves). I take a lot of inspiration from the Bootstrappable project for this sort of thing. The other thing that can be done is to translate the proof to another proof system. This allows you to turn an MM0 proof of MM0 correctness into an MM/Lean/Isabelle proof of MM0 correctness. This doesn't make it any less circular, but with multiple bootstraps you only have to trust one of them, and if you are predisposed to trust a particular proof assistant then this might be more psychologically satisfactory. (But I want to emphasize that all these proof systems are all still running on your (say) x86 hardware, so a bug in the hardware affects them all.) Basically, self-verification is not a substitute for all the other, traditional methods for ensuring code correctness, namely looking at the code, reimplementing it in several languages, unit testing and so on. However, it is far more reliable, especially when you combine a cursory inspection with a formal proof (where the cursory inspection is there to eliminate the equivalent of trusting trust attacks). Is it more of a strengthening exercise where you can't be sure that it's > verified but the probability of MMC having a mistake and then MM0 having a > mistake becomes super low or something? > MMC doesn't have to be verified either, because it, like MM1, is proof producing. The only thing that has to be trusted is the MM0 kernel and the definition of x86, because MMC produces proofs of correctness relative to that definition of x86 that will be checked by the MM0 kernel. But since the program being checked is the MM0 kernel, we have the circularity as described above. If you're interested in answering, and I can totally understand if you're > not, could you go easy on me when explaining? I get easily confused. > Thanks, Jon. > I of course am quite happy to answer these questions at length (sometimes too much length :P ), and appreciate the interest in my work. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvsMLWWUEjurWHz7748J-%3DKBHEwpV1KksoT73bfOGzabg%40mail.gmail.com.
