Metamath C

[Mario Carneiro]

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

[Giovanni Mascellani]

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:

> --
> 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 metamath+u...@googlegroups.com
> <mailto:metamath+u...@googlegroups.com>.
> 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 <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[OlivierBinda]

I'm also following what is going on for MM0 from far away (teaching with
covid19 just ended, building a house just started, got to refactor and
publish an update for an android app to save it from bit-rot)

I don't think that I'll ever meddle with metamath-C but I'll definetely
read about it and resume work on MM0-based stuff in a few months (and I
will be among those that profit from MM0 to Metamath translation)


Meanwhile, I'll just cheer everyone
Great work,
Best regards,
Olivier