Borrow checking in a-mir-formality

[nikomatsakis]

Metadata
Point of contact	@nikomatsakis
Team(s)	types
Goal document	2025h2/a-mir-formality

Summary

Extend a-mir-formality with the ability to represent function bodies as MiniRust programs; a type checker based on the MIR type checker from the compiler; and a model that covers key parts of the the Polonius Alpha proposal.

Tasks and status

• Implementation of MiniRust integration (@tiif)
• Implementation of MIR type checker (@tiif)
• Implementation of Polonius Alpha model (@tiif)
• Standard reviews (types )
• Dedicated reviewer (types )
• Mentorship (@nikomatsakis)

---

Note: we have updated the body to match the 2025h2 goal. Your original text is preserved below.

Metadata
Point of contact	@nikomatsakis
Team(s)	types
Goal document	2025h1/formality

Summary

We will model coherence (including negative impls) in a-mir-formality and compare its behavior against rustc.
This will require extending a-mir-formality with the ability to run Rust tests.

Tasks and status

• Discussion and moral support (types )

Modeling and documenting coherence rules

• Author explainer for coherence model (@nikomatsakis)

Running Rust tests in a-mir-formality

• Mentorship (@nikomatsakis)
• Implementation ()

Stretch goal: modeling Rust borrow checker

• Mentorship (@nikomatsakis)
• Implementation ()

[nikomatsakis]

This issue is intended for status updates only.

For general questions or comments, please contact the owner(s) directly.

[nikomatsakis]

Key developments:

• Landed fuzzing infrastructure but not using it for anything.
• There have been some contributors opening PRs (🎉) but due to vacation and other things I haven't gotten back to them very well.

Next steps:

• Engage contributors
• Begin work towards loading test cases from stable-mir as well as modeling polonius (to tie in with Stabilizable Polonius support on nightly #118).

[nikomatsakis]

I think it's pretty clear that this goal never really happened. I'm still keen to see progress on building community around a-mir-formality but I overestimated my capacity (shocker). I'm going to close it for now but I plan to make up some plans for next session.

[nikomatsakis]

This is a continuing project goal, and the updates below this comment will be for the new period 2025h1

[nikomatsakis]

I have established some regular "office hour" time slots where I am available on jitsi. We landed a few minor PRs and improvements to the parser and oli-obk and tif have been working on modeling of effects for the const generics work. I'm planning to start digging more into the modeling of coherence now that the basic merging is done.