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
Le 24/06/2020 à 09:36, Giovanni Mascellani a écrit :
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>.
--
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/f528a5e4-e80f-507d-bf06-ed8c01715da7%40gmail.com.
