Type Theory for the Working Rustacean
summary
Shows exactly how Rust’s type system is used to mimic dependent types: defines a type-level natural via a gnat trait, implements a size-proof Vec that carries its length in the type, and replaces copy_from_slice with a copy_from_proven_slice that uses a less_or_equal trait (associated type result = true) so mismatched lengths fail at compile time. Demonstrates push that increments the type-level length and claims this pattern avoids runtime crashes that once cost a day and a half of debugging.
AI-written summary · about
chapters (4)
related talks
25mType System Tips for the Real World
31mThe Rust That Could Have Been
33mRust and Haskell, sitting in a tree
26mThe Freedom of Static Typing
36mRust's trait system is a proof engine, let's make it prove us an ABI!
38mType-level interfaces in Haskell & Rust: pragmatic type-level programming
29mExtending Rust’s notions of sizedness
54mSubtyping in Rust and Clarke's Third Law