Hi all, It's been a while since I've talked about MM0 on the board. I've made a lot of progress, and the MM0 paper (https://arxiv.org/abs/1910.10703) is bigger and better than ever and a version of it is to appear at the CICM conference this year. But we're entering a new phase of development, and with it comes another language design: Metamath C! Because it's more like a programming language than a proof language I'm asking the PL folks to chime in over at https://www.reddit.com/r/ProgrammingLanguages/comments/hczeof/metamath_c_a_language_for_writing_verified/?utm_source=share&utm_medium=web2x and in the interest of not bifurcating discussion I would suggest people make language comments there.
As you may already know, MM0 is a proof language similar to metamath but optimized for specifications, and MM1 is a proof assistant for MM0. That proof assistant has a metaprogramming language based on scheme, and in that language we expose a new function called mmc-compiler that accepts an s-expression input. The language of that input is MMC. It is vaguely styled after C but allows you to perform proofs in separation logic using program flow to pass around proofs of separating propositions over the program state. I've written a language design document here: https://github.com/digama0/mm0/blob/master/mm0-rs/mmc.md , and you can see a code sample at https://github.com/digama0/mm0/blob/master/examples/verifier.mm1 . If you would like to make changes to the language structure, now is the time! Mario Carneiro -- 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/CAFXXJSvR8H54HWcH_7CaxZgdrd-RphUvsSPzn2mMinDOq8gy%2BA%40mail.gmail.com.
