Rust's Trait System as a Proof Engine for ABI Generation

Dive into an advanced exploration of Rust's trait system and its capabilities as a proof engine in this 36-minute conference talk from RustLab. Learn how to leverage const generics for mathematical operations, influence type layouts based on generic parameter sizes, and create lists, loops, ternaries, and branches without declaring functions. Discover the inner workings of 'stabby' and its stable representation for enums. Explore the use of Generic Associated Types (GATs) to perform computations without encountering where-clause complexities. Uncover the techniques behind the first stable ABI in Rust with niche optimizations, and gain insights into pushing the limits of Rust's Turing-complete type system. Starting with essential context and background concepts, the talk progresses to a code-oriented session, revealing the potential and intricacies of Rust's powerful trait system.

Rust's trait system is a proof engine, let's make it prove us an ABI! - Pierre Avital