Performant, Readable and Interoperable Rust from Dafny
summary
A Dafny-to-Rust compiler that emits largely readable Rust code, uses a postprocessing pass to reuse local names and factor absolute paths into imports, and proves its identifier encoding injective as part of CI (injective mapping lemma in CI). Memory model uses nullable raw pointers, RC + RefCell semantics lowered to unsafe wrappers and zero-cost Option encodings, with mutable reference counting for the encryption SDK. Published mid‑July, it shows 9 of 10 benchmarks ≤22% slower with 2 matches to native while yielding 20% code reduction in the encryption SDK.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:06Compile Dafny to Rust
- 3:13Readability of identifiers
- 5:42Simplify module paths
- 7:07References without GC
- 10:39Inheritance and coercion
- 11:40Initialization tracking
- 13:29Extern and extend methods
- 14:36Performance and readability
- 15:21Q&A
