rust-lang/chalk

An implementation and definition of the Rust trait system using a PROLOG-like logic solver

Source code at GitHub https://rust-lang.github.io/chalk/book/

{
  "createdAt": "2015-07-26T10:13:23Z",
  "defaultBranch": "master",
  "description": "An implementation and definition of the Rust trait system using a PROLOG-like logic solver",
  "fullName": "rust-lang/chalk",
  "homepage": "https://rust-lang.github.io/chalk/book/",
  "language": "Rust",
  "name": "chalk",
  "pushedAt": "2025-08-29T20:45:26Z",
  "stargazersCount": 1976,
  "topics": [],
  "updatedAt": "2025-11-25T03:50:05Z",
  "url": "https://github.com/rust-lang/chalk"
}

chalk

Chalk is a library that implements the Rust trait system, based on [Prolog-ish][Prolog] logic rules.

See the Chalk book for more information.

FAQ

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 Vec<u32> implement 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][chalk-lowering-details].

Where does the name come from? chalk is named after [Chalkidiki], the area where [Aristotle] was born. Since Prolog is a logic programming language, this seemed a suitable reference.

[Prolog] !: https://en.wikipedia.org/wiki/Prolog [Chalkidiki] !: https://en.wikipedia.org/wiki/Chalkidiki [Aristotle] !: https://en.wikipedia.org/wiki/Aristotle [chalk-lowering-details] !: https://rust-lang.github.io/chalk/book/#chalk-works-by-converting-rust-goals-into-logical-inference-rules

Blog posts

[blog-posts] !: #blog-posts 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

REPL

There is a repl mainly for debugging purposes which can be run by cargo run. Some basic examples are in [libstd.chalk]!(libstd.chalk):

$ cargo run
?- load libstd.chalk
?- Vec<Box<i32>>: Clone
Unique; substitution [], lifetime constraints []

Contributing

If you’d like to contribute, consider joining the [Traits Working Group][working-group]. We hang out on the [rust-lang zulip][rust-lang-zulip] in the [#wg-traits][wg-traits-stream] stream.

See [the contributing chapter][contributing] in the chalk book for more info.

[working-group] !: https://rust-lang.github.io/compiler-team/working-groups/traits/ [rust-lang-zulip]: https://rust-lang.zulipchat.com [wg-traits-stream] !: https://rust-lang.zulipchat.com/#narrow/stream/144729-wg-traits [contributing] !: https://rust-lang.github.io/chalk/book/contribution_guide.html