Chalk is a library that implements the Rust trait system, based on Prolog-ish logic rules.
See the Chalk book for more information.
How does chalk relate to rustc? The plan is to have rustc use the
chalk-solve crate (in this repo) to answer questions about Rust programs, for example, "Does
Debug?". Internally, chalk converts Rust-specific information into logic and uses a logic engine to find the answer to the original query. For more details, see this explanation in the chalk book.
Here are some blog posts talking about chalk:
- Lowering Rust Traits to Logic
- Explains the basic concepts at play
- Unification in Chalk, Part 1
- An introduction to unification
- Unification in Chalk, Part 2
- Extending the system for associated types
- Negative reasoning in Chalk
- How to prove that something is not true
- Query structure in chalk
- The basic chalk query structure, with pointers into the chalk implementation
- Cyclic queries in chalk
- Handling cyclic relations and enabling the implementation of implied bounds and other long-desired features in an elegant way
There is a repl mainly for debugging purposes which can be run by
cargo run. Some basic examples are in libstd.chalk:
$ cargo run ?- load libstd.chalk ?- Vec<Box<i32>>: Clone Unique; substitution , lifetime constraints 
See the contributing chapter in the chalk book for more info.