leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: Program verification

Topic: Metamath C


Mario Carneiro (Jun 21 2020 at 03:14):

For anyone who likes language design and would like to help me in the next phase of the MM0 project, I am soliciting comments in the Reddit PL forum for the new Metamath C language. In summary, it is a programming language for writing functionally correct programs with respect to rock bottom semantics. Any comments welcome (here or there)!


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll