Synthesizing Loop-Free Programs with Rust and Z3 (2020)
Summary
Nick Fitzgerald's 2020 post explores program synthesis, specifically counterexample-guided iterative synthesis (CEGIS) for loop-free, component-based programs using Rust and the Z3 SMT solver. It covers formalization, SMT queries, verification, finite synthesis, and location mappings, and walks through a concrete isolating-the-rightmost-zero-bit example. The article also documents an end-to-end Rust implementation and discusses results and challenges, including performance cliffs with larger problems.