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? 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. 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? 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. -- 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/020926cd-3f0d-4324-ae4d-772b17f36149o%40googlegroups.com.
