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.