Well, I took a stab at this in my initial announcement, but perhaps that was not the correct level of detail. At the biggest picture, I want Rust's trait checker to be a thing of beauty -- efficient, well-specified with clean and clear semantics, and with a relatively high
bus factor
to boot.
A bit more detailed, the rough plan is still the "Chalk plan":
- Map Rust's traits to logic clauses that roughly correspond to Lambda Prolog, roughly as described in my first Chalk blog post -- though the details have evolved since then.
- Solve these traits with an efficient solver, hopefully one that is quite a bit factored out so as to be independent of rustc. Probably following the on-demand SLG solver model laid out here, but I wouldn't be surprised if that evolves some more as well.
(The reason I would like the solver to be independent of rustc is basically to make it easier to understand and to help encourage contribution (smaller codebases being more approachable). Also, if all goes well, this code be a shared resource used by e.g. IDEs or other tooling. But independence is ultimately a longer term goal, not something I expect to reach immediately.)
OK, time for bed, but I hope that gives some idea.