Rust's trait system is a proof engine, let's make it prove us an ABI!
summary
Claims that Rust's trait system can do real computation to produce a stable ABI and demonstrates a working crate that does it. It uses GAT-powered proofs and typenum-style type arithmetic to implement addition, multiplication and layout math at compile time, produces a stabby crate that emits layout reports and performs deterministic niche packing for enums, and supports multitraits and a stable allocator API. It runs on GAT-capable Rust, costs extra compile time (previously ~1s per enum before optimizations), is usable for Rust-to-Rust plugins now and has a spec for cross-language implementations.
AI-written summary · about
chapters (29)
- 0:00Introduction
- 1:08Counting with Rust traits
- 2:12Traits as functional types
- 3:37Collections and numbers
- 4:42Typenum limitations
- 5:46Generic Associated Types
- 6:50Defining booleans and TyFu
- 8:14TyFu recursion limits
- 9:18Unsigned integers and circuits
- 10:42Type-level addition and multiplication
- 11:23Runtime types and conversions
- 13:13Scientific computing with tensors
- 13:36Memory management and slabs
- 14:39ABI fundamentals
- 16:24C ABI quirks
- 18:09Rust ABI stability
- 19:55Dynamic linkage and plugins
- 21:41Introducing Stabby
- 23:28Stabby implementation
- 24:33Type system tips
- 26:19Conclusions and limits
- 27:25Q&A
- 27:45Questions on pack types
- 28:54Cross-language ABI stability
- 29:57ABI interpretation reports
- 31:24Comparison with stable ABI RFC
- 32:43Compile-time overhead
- 34:10Consteval expressions
- 35:15Type system advances
related talks
26mCompile-Time Authorization
49mThe Eternal Sunshine of the Spotless Programming Language
10mAutomatically Enforcing Rust Trait Properties
19mType Theory for the Working Rustacean
31mThe Rust That Could Have Been
01h 14mRust: A Friendly Introduction
25mType System Tips for the Real World
01h 11mDuck-Tape Chronicles - Rust C++ Interop