Model coherence in a-mir-formality

[nikomatsakis]

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 Scalable 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.