Github
文档a-mir-formality
这个仓库是一个早期阶段的实验项目，旨在成为Rust MIR的完整、权威的形式化模型。假设这些实验取得成果，目标是将这个模型作为RFC引入Rust，并将其作为语言定义的官方部分进行开发。
快速入门指南
像任何Rust项目一样：
- 克隆
cargo test --all
形式化层次
形式化结构分为几个层次。这些层次也旨在与chalk和最终的Rust特征求解器实现紧密对应。理想情况下，应该能够在形式化和代码之间轻松地进行映射。
- formality-check：定义了检查Rust程序的顶层例程。
check_all_crates实际上是main，所以它是一个很好的阅读起点。 - formality-core：定义了日志宏。
- formality-macros：定义了过程宏，如
#[term]以及各种派生宏。这些用于生成解析、美化打印、折叠等的样板代码。 - formality-prove：定义了证明目标的规则（例如，这个特征是否已实现？）
- formality-rust：这是"Rust声明"层，定义了Rust的"顶层项"及其语义。这包括crate、结构体、特征、实现，但不包括函数体。
- formality-types：这是"类型"层，定义了Rust类型和用于等价/关联它们的函数。表示方法旨在涵盖所有Rust类型，但优化了提取它们的"基本属性"。
