Hi Mario, the work you are doing on MM0 is wonderful. I wish I had more time to follow and maybe contribute, but I need to care about other commitments right now (including the birth of a daughter, quite a time consuming business). Keep up the good work, I hope to be able to catch up one day.
(although I admit it's hard to keep the FOMO at bay...) Giovanni. Il 21/06/20 05:05, Mario Carneiro ha scritto: > 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] > <mailto:[email protected]>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAFXXJSvR8H54HWcH_7CaxZgdrd-RphUvsSPzn2mMinDOq8gy%2BA%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJSvR8H54HWcH_7CaxZgdrd-RphUvsSPzn2mMinDOq8gy%2BA%40mail.gmail.com?utm_medium=email&utm_source=footer>. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/eea7dbc8-417a-8589-9b03-d5d54f0954ea%40gmail.com.
signature.asc
Description: OpenPGP digital signature
