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. 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. 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. 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? 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. Mostly I’d just like to be encouraging, what you’re doing is incredible. I think formal methods are definitely the future. -- 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/7a6dd14a-3b6b-4480-b9af-59d3bce6e984o%40googlegroups.com.
