Metamath Zero (a formal logical framework) in Rust

MM0 is a specification-only language, and it is paired with proofs with a defined theory but an implementation-defined concrete syntax. It was inspired by Metamath (a logical framework) and Lean (an interactive theorem prover, similar to Coq).

It has a few implementations in a different languages and, of course, there is a Rust one - mm0-rs.

This is how (only a part) a "hello world" looks like:

-- Declare a string sort constructed from contatenating singleton
-- strings and empty strings. The `sadd` function is treated by
-- the verifier as associative.
strict free sort string;
term s0: string;
term s1: char > string;
term sadd: string > string > string; infixr sadd: $+$ prec 50;

-- All the above terms and sorts must be declared with exactly these types,
-- or `input string` and `output string` will not work. But we are still
-- a long way from being able to write strings in any reasonable way.
-- Let's define some codes for ASCII characters:

def nl: string = $ s1 (ch x0 xa) $; -- new line
def __: string = $ s1 (ch x2 x0) $; -- space
def bang: string = $ s1 (ch x2 x1) $; -- exclamation point
prefix bang: $_!$ prec max;

def _H: string = $ s1 (ch x4 x8) $;
def _W: string = $ s1 (ch x5 x7) $;
def _d: string = $ s1 (ch x6 x4) $;
def _e: string = $ s1 (ch x6 x5) $;
def _l: string = $ s1 (ch x6 xc) $;
def _o: string = $ s1 (ch x6 xf) $;
def _r: string = $ s1 (ch x7 x2) $;

output string: $ _H + _e + _l + _l + _o + __ +
                 _W + _o + _r + _l + _d + _! + nl $;

DISCLAIMER: Project is not mine, just wanted to share.

1 Like

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.