On Wed, Aug 5, 2020 at 4:09 AM Jon P <[email protected]> wrote: > Awesome Mario, thanks for the response, it takes me a few days to respond > because I have to think a lot ha ha. > > I can see how fully symbolic proofs are better. I can also see how you > arrived at this place if separation logic has been implemented in COQ and > HOL, it feels like a big step from MM. > > It makes sense too that x86 can be formally specified. I think it’s really > clever that the compiler can progressively refine the proof down to lower > levels, this lets the humans just read the high level stuff which is cool. > Do you have the x86 definitions in a file somewhere? I’d be interested to > see them, though may well not understand. >
Indeed I do: https://github.com/digama0/mm0/blob/master/examples/x86.mm0 It would be better with syntax highlighting but you will need to open it in vscode for that. > Can I ask what the relationship between MM1 and MMC is? For example if I > am writing a program in MMC can I use MM1 to help me produce the high level > proof for the program or is MM1 more a tool for making MM0 proofs only? I > imagine some sort of proof assistant for MMC would be helpful. > MMC is a DSL inside MM1. That means that an MMC program is written as the input to a tactic running in MM1. For example, https://github.com/digama0/mm0/blob/master/examples/verifier.mm1 contains the draft of the MM0 verifier in MMC. The code is all MM1 until line 38, when we enter what is essentially a big quoted expression within which the language is changed to MMC and you start seeing keywords like "proc" and "typedef" more reminiscent of C than a proof language. In certain places, like at the _ on line 69, a proof is expected, and this proof has the same format as the usual MM1 proofs. The compiler will specially prepare a proof context so that even though you are actually inserting a bit of proof in the middle of the giant proof the compiler is working on, you don't see any of that and you only have the facts that you request so as to not make it overwhelming. When you are in these little proofs, you can use all the usual tools that MM1 provides. Alternatively, if the theorem is quite heavyweight and you don't want to embed it in the middle of the MMC program, you can interrupt the program between any top-level items (i.e. at the beginning of the function), finish the tactic invocation and the do block and then write a theorem in MM1 just like one writes pure mathematical theorems, give the proof, then return to MMC and refer to the theorem in the mini proof block where it is needed. I am also curious as to what else you want to use MMC for, it feels like > you’re building a whole, very sophisticated, programming language just to > write one program in it (MM0). Do you have other ideas for projects? I can > imagine there are a lot of applications for things like aerospace, > cryptography and finance etc where people need really robust code. > Ha, you noticed. I will try to keep the sophistication down for the first draft because it's definitely possible to overengineer in this area, and this was specifically something I wanted to avoid. But I'm also doing a PhD dissertation with this project and want to make sure I get something independently useful even if the MM0 verification turns out to take longer than expected. > How far through implementing all this are you? I know you’ve done quite a > lot of it which is impressive. What are your next steps? > The MMC implementation is just starting. I have just started on the typechecker, which is responsible for doing type inference and passing around typing proofs in the separation logic, but I also haven't written any of the proof support that the compiler needs yet, for example the separation logic itself hasn't even been defined yet, and I'm waiting to see the shape of the lemmas that the compiler requires before writing that so that I can be sure it is accomplishing the task set to it (and no more). There is also still some pure MM1 work to be done to prove x86.mm0 and mm0.mm0, which mostly entails proving the existence of various kinds of inductive types. This is the sort of thing that every proof assistant automates eventually, so I'm not sure if it's worth it to push through the 10 or so inductive datatypes I need by hand, or write the tactic to solve them all (which is usually worthy of a research article on its own but is a considerable time sink). In metamath we never bothered to automate this kind of thing, possibly because there were never enough CS-themed projects to necessitate recursive data structures built out of disjoint union and cartesian product. But these are extremely common in programming languages (they are called "algebraic data types"), and they are useful for modelling syntax, for example you might define the collection of all propositional logic expressions as: inductive prop_expr | imp : prop_expr -> prop_expr -> prop_expr | not : prop_expr -> prop_expr | var : NN0 -> prop_expr and from this specification, the datatype compiler will generate a type "prop_expr" with functions "imp", "not", "var" with the stated types, as well as a recursion and induction principle for defining functions by structural recursion and proving properties by structural induction, for example |- A. a e. prop_expr A. b e. prop_expr (P [a / x] -> P [b / x] -> P [imp a b / x]) /\ A. a e. prop_expr (P [a / x] -> P [not a / x]) /\ A. n e. NN0 P [var n / x] -> A. x P for the induction principle, and |- rec_prop_expr I N V (imp a b) = I a b (rec_prop_expr I N V a) (rec_prop_expr I N V b) |- rec_prop_expr I N V (not a) = N a (rec_prop_expr I N V a) |- rec_prop_expr I N V (var n) = V n for the recursion principle. The work being done now in set.mm on well founded recursion along general well founded orders is the first baby step in this direction but we're quite far from having the whole thing automated away in MM. Also do you want any help? I am 99% sure I don’t have any skills which > could be of use to you and I am trying to help with the OpenAI proof > assistant a bit when I have energy so I don’t think I will be able to help > much. However I do love this field so want to get more into it and if > others are reading this they may be interested too. > I have a bunch of proofs to be done, which I could outsource if anyone is interested. For example x86.mm1 currently contains a huge number of fairly simple theorems that have been stated and not proved, so it's fairly straightforward to get into it if you (or others) are interested. You would have to learn the MM1 language, but that's not a terrible side effect, and I would be happy to help with onboarding any way I can. > Mostly I’d just like to be encouraging, what you’re doing is incredible. I > think formal methods are definitely the future. > Thanks! 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/CAFXXJSue80gt1UQCf4m7Y5ibe0g__Enb9gx1GQ5ROSr%3DOA1XEg%40mail.gmail.com.
