 # 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.