This repository is an early-stage experimental project that aims to be a complete, authoritative formal model of the Rust MIR. Presuming these experiments bear fruit, the intention is to bring this model into Rust as an RFC and develop it as an official part of the language definition.
Like any Rust project:
- Clone
cargo test --all
Check out a-mir-formality book for an overview and introduction to a-mir-formality.
Formality is structured into several layers:
- formality-macros: Defines procedural macros like
#[term]as well as various derives. These are used to generate the boilerplate code for parsing, pretty printing, folding, etc. - formality-core: Language-independent foundation for formal semantics — variable binding, the judgment/proof system, fixed-point computation, and collections.
- formality-rust: The Rust-specific model. Contains
grammar/(AST definitions),check/(semantic checking, withcheck_all_cratesas the entry point), andprove/(trait solving and type normalization).