Program synthesis

Program synthesis can be categorized by the type of specification and the search strategy. Deductive synthesis, pioneered by Cordell Green and Zohar Manna, derives programs from formal proofs of correctness. Inductive synthesis, also called programming by example (PBE), infers programs from input-output pairs, often using search over a grammar of candidate programs. Counterexample-guided inductive synthesis (CEGIS) iteratively refines a candidate program by testing it against counterexamples. Modern tools often use SAT/SMT solvers to explore the search space efficiently.²

Program synthesis has practical applications in end-user programming, such as the FlashFill feature in Microsoft Excel, which automatically generates string transformation functions from examples. It is also used in automated program repair, where it generates patches for software bugs, and in hardware design, where it synthesizes circuits from high-level specifications. In education, tools like the Automata Tutor help students learn by synthesizing feedback. Additionally, synthesis is used in database query generation and in robotics for generating control programs.³

Despite progress, program synthesis faces significant challenges. The search space of possible programs is often infinite, requiring clever heuristics and constraints. Scalability remains an issue for large-scale programs. Ambiguity in specifications, especially from natural language, can lead to incorrect programs. Moreover, synthesizing programs that are not only correct but also efficient and readable is difficult. Recent research explores using deep learning to guide the search, but these methods require large datasets and may not guarantee correctness.⁴

Beyond mainstream applications, program synthesis has niche uses. In computational biology, it helps design genetic circuits. In cryptography, it synthesizes protocols that are resistant to attacks. The concept of synthesis of reactive systems from temporal logic specifications, introduced by Amir Pnueli, has applications in controller design. Also, the Sketch system uses partial programs with holes, allowing programmers to specify high-level structure while the tool fills in details. The field has roots in the calculus of communicating systems and the Curry-Howard correspondence, linking proofs and programs.⁵

Inductive synthesis

Inferring a program from input-output examples.

CEGIS

Counterexample-guided inductive synthesis, an iterative refinement loop.

SMT solver

Satisfiability modulo theories solver, used to reason about logical formulas.