hackaugusto / a-mir-formality

a model of MIR and the Rust type/trait system

a-mir-formality

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.

Quickstart guide

Like any Rust project:

• Clone
• cargo test --all

Layers of formality

Formality is structured into several layers. These layers are meant to also map fairly closely onto chalk and the eventual Rust trait solver implementation. Ideally, one should be able to map back and forth between formality and the code with ease.

• formality-check: Defines the top-level routines for checking Rust programs. check_all_crates is effectively the main, so it's a good place to start reading.
• formality-core: Defines logging macros.
• 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-prove: Defines the rules for proving goals (e.g., is this trait implemented?)
• formality-rust: This is the "Rust declarations" layer, defining Rust "top-level items" and their semantics. This includes crates, structs, traits, impls, but excludes function bodies.
• formality-types: This is the "types" layer, defining Rust types and functions for equating/relating them. The representation is meant to cover all Rust types, but is optimized for extracting their "essential properties".