Leveraging Rust Types for Program Synthesis
summary
First deductive synthesizer for safe Rust that uses Rust types to both shrink specifications and prune search, extracting programs from proofs and guaranteeing well-typed code that meets specs. The implementation RusSOL embeds a new program logic Synthetic Ownership Logic and synthesizes 115 of 117 annotated functions, averages 5.4 LOC, produces a 24-line rose-tree flatten in ~10s, and generates about 3,000 lines from top crates; failures stem from required unsafe code or nontrivial arithmetic synthesis.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:22Program synthesis overview
- 1:03Rust types for code gen
- 2:05Live Russell demo
- 6:25How Russell synthesizes
- 7:08Synthetic Ownership Logic
- 11:02Russell performance eval
- 13:51Type correctness guarantees
- 14:55Key contributions
- 15:16Q&A
related talks
19mA Hybrid Approach to Semi-automated Rust Verification
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
25m"Compiler-Driven Development: Making Rust Work for You"
56mReady for Rust
31mGetting Something for Nothing
19mCrabtree: Rust API Test Synthesis Guided by Coverage and Type
15mTranslating C to Safer Rust
21m“Fearless Refactoring & the Art of Argument-Free Rust”