Program Synthesis: Foundations & Trends (Survey by Gulwani et al., 2017) – A comprehensive 130-page survey covering the state of the art up to 2017 (Program Synthesis in 2017-18 – Alex Polozov) (Program Synthesis in 2017-18 – Alex Polozov). It overviews all major paradigms (enumerative search, constraint-based, type-directed, stochastic, and neural methods) and applications (from end-user programming to education). A perfect entry point for newcomers, written by leading researchers Sumit Gulwani, Rishabh Singh, and Alex Polozov. (Open access PDF available) (Program Synthesis in 2017-18 – Alex Polozov).
Historical Overviews: Program synthesis has deep roots in AI. Early seminal works include Manna and Waldinger (1971) on deductive synthesis from formal specs ((PDF) Toward Automatic Program Synthesis) and research on automata-theoretic synthesis by Church, Büchi, and Landweber (1960s) ([#84: Could Program Synthesis Unlock AGI?
by Ksenia Se
Medium](https://kseniase.medium.com/84-could-program-synthesis-unlock-agi-45a43b04d4f4#:~:text=,%E2%80%9D)). A Medium essay by K. Sen (2023) provides an accessible history from Turing’s 1945 memo through formal methods in the 1980s, up to modern developments ([#84: Could Program Synthesis Unlock AGI?
by Ksenia Se
Medium](https://kseniase.medium.com/84-could-program-synthesis-unlock-agi-45a43b04d4f4#:~:text=History%3A%20Of%20course%2C%20we%20can,trace%20Program%20Synthesis%20way%20back%E2%80%A6)) ([#84: Could Program Synthesis Unlock AGI?
by Ksenia Se
Medium](https://kseniase.medium.com/84-could-program-synthesis-unlock-agi-45a43b04d4f4#:~:text=,holes%20that%20are%20automatically%20filled)). It highlights how initial logic-based approaches gave way to more practical methods in later decades.
“Deductive Program Synthesis”: Manna & Waldinger (1980) – A classic paper (ACM TOPLAS) formalizing the deductive approach, where programs are derived by proving the existence of a solution that meets a specification. This work established the paradigm of treating program synthesis as theorem proving – an idea that influenced later formal methods and the development of tools in the 1980s and 90s.
Inductive Logic Programming (ILP) – Muggleton et al. (1990s): ILP is an early form of inductive program synthesis in the machine learning community. It focuses on learning logic programs (Prolog rules) from examples and background knowledge (Inductive logic programming - Wikipedia). For instance, the ILP system FOIL (Quinlan) and PROGOL (Muggleton) could synthesize recursive logic predicates from training data. ILP connects AI with program synthesis and laid groundwork for later data-driven and neural approaches.
Genetic Programming – Koza (Book, 1992): John Koza’s Genetic Programming introduced evolutionary search for programs, treating program code as the “genome” to be mutated and crossed over. While not always categorized under program synthesis in the PL sense, this line of work demonstrated stochastic synthesis of programs (often expression trees) and solved simple problems via natural selection. It’s a foundational work for stochastic and evolutionary approaches to synthesizing programs.
“Sketching” – Solar-Lezama’s PhD thesis (2008) – This thesis (MIT) introduced the idea of program sketching, where a developer provides a partial program with “holes” and the synthesizer fills in the holes with code that meets a spec. The approach, implemented in the SKETCH system, uses constraint solving (SAT/SMT) to complete code. Sketching made synthesis more practical for real programming tasks by allowing users to guide the search. (This work received the ACM Doctoral Dissertation Award.) ([#84: Could Program Synthesis Unlock AGI?
Syntax-Guided Synthesis (SyGuS) – Alur et al. (2015) – This paper formalized the SyGuS paradigm ([#84: Could Program Synthesis Unlock AGI?
by Ksenia Se
Medium](https://kseniase.medium.com/84-could-program-synthesis-unlock-agi-45a43b04d4f4#:~:text=%2A%20Modern%20Resurgence%20%282010s,to%20guide%20the%20synthesis%20process)). The idea is to constrain the program search with a grammar/template that defines the space of allowed implementations, while also given a logical spec for correctness (Review: Syntax-Guided Synthesis :: Reasonably Polymorphic). By guiding the search syntactically, one can more efficiently synthesize programs. The SyGuS formulation led to an annual competition (SyGuS-Comp) and spurred development of solver-based synthesizers. (See also: SyGuS-Comp 2018 report ([1904.07146] SyGuS-Comp 2018: Results and Analysis - arXiv) for results and solver progress).*
Neural Program Synthesis Surveys (2021–2023): Several survey papers and articles have emerged summarizing the intersection of deep learning and program synthesis. E.g., “Program Synthesis with Large Language Models” (Preprint 2023) situates code-generation transformers (like OpenAI Codex) in the context of synthesis ((PDF) Toward Automatic Program Synthesis) ((PDF) Toward Automatic Program Synthesis).) and “Neural Program Synthesis” (Ellis et al., 2021) reviews approaches where neural networks learn to produce programs (covering sequence-to-sequence models, neurally guided search, etc.). These resources help bridge classical synthesis and modern AI-driven techniques.