Learn · Intermediate

Program synthesis: making a computer write the program from the specification

Program synthesis is the automated construction of a program that satisfies a specification—examples, tests, types, constraints, or a formal statement of what the program must do. It matters because it changes the programming task from spelling out every instruction to defining a target behavior that a machine can search for and verify. When the specification is strong, synthesis can produce code with a clearer correctness story than an untested code completion.

Most programming starts with an intention and ends with code. You want to extract a date, validate an invoice, schedule a job, or transform a data format. You translate that intention into loops, conditionals, data structures, and error handling. Program synthesis asks whether the computer can perform more of that translation. Give it enough evidence about the behavior, and it searches through possible programs for one that fits.

The simplest specification is a set of examples. If a user gives John Smith → Smith, John and Ada Lovelace → Lovelace, Ada, a synthesizer can search for a transformation that explains both. Microsoft Research's Flash Fill paper, by Sumit Gulwani, made this idea familiar through spreadsheet transformations: a few input-output examples could generate a small program that repeated the pattern across a column. The magic was not a model guessing prose. It was a carefully chosen language of string operations and a search procedure that found programs consistent with the examples.

That last phrase—consistent with the examples—is the strength and the trap. Many programs may match two examples. A program that swaps the first and last words works for the names above, but what happens with “Mary van der Meer,” a one-word name, or a title? The examples are a partial view of intent. Good synthesis systems therefore use more than examples when they can: type constraints, domain-specific rules, property tests, user interaction, and ranking that favors simple understandable programs.

A useful analogy is a courtroom sketch artist. A witness describes height, hair, glasses, and a scar; the artist produces a face that satisfies those constraints. If the description is vague, many faces fit. If it includes a clear photograph, there is little ambiguity. The synthesizer is not reading the developer's mind. It is narrowing a space of possible programs using the evidence provided.

There are several major ways to do this. Enumerative synthesis tries candidate programs one by one, usually in order of increasing simplicity, until one passes the specification. Constraint-based synthesis turns the task into a problem for a solver: choose the expression pieces and their values so that all examples or logical assertions hold. Syntax-Guided Synthesis, introduced by Rajeev Alur and colleagues, formalized a productive middle ground: specify not just the desired behavior but a grammar of legal implementations. That grammar keeps the search from wandering into an infinite universe of code and can encode important design restrictions.

Deductive synthesis works from logical proofs, deriving a program as evidence that a specification is satisfiable. Inductive synthesis works from examples. Stochastic or neural synthesis uses learned probabilities to prioritize promising candidates. The boundaries blur in modern systems. A language model can propose a useful sketch, an enumerator can fill its holes, a compiler can type-check it, and tests or a theorem prover can reject failures. This is a more dependable picture of AI coding than “the model writes the program”: generation supplies hypotheses; specifications and verifiers decide which hypotheses survive.

That framing connects directly to the day's Compile by Training news. That system takes a natural-language specification, asks teachers to generate examples, and trains a small task-specific neural adapter. It resembles program synthesis in spirit because it compiles a general instruction into a reusable specialized function. But it differs in a crucial way: a classical synthesizer returns explicit code whose behavior can often be exhaustively checked against a small language; a neural adapter remains probabilistic. It should be tested and surrounded by validation, especially in high-stakes contexts.

Synthesis becomes most powerful when there is a cheap, trustworthy verifier. If every candidate can be run against a large test suite, checked against a type system, or proven to meet a formal contract, then trying thousands of candidates is cheap. This is why it works well for string transforms, query construction, small algorithms, hardware blocks, and formal proofs. It is also why it struggles with “make the website feel premium” or “write an inspiring essay”: those requests have no crisp oracle for correctness. Constrained decoding is related at generation time—it restricts what output a model can emit—but it is not synthesis by itself.

The honest caveat is specification debt. A synthesized program can be perfectly correct with respect to the wrong specification. A tax calculator that passes every supplied example but lacks a rule for a new jurisdiction is not safe. In safety-critical work, synthesis should make missing requirements easier to discover, not create false confidence. The discipline is to write adversarial examples, state invariants, keep the generated artifact readable where possible, and re-run the verification suite whenever requirements change.

The deeper lesson is liberating: code is not the only useful interface to a computer. Examples, constraints, types, tests, and formal goals are also programming languages of a kind. Program synthesis is the machinery that turns those higher-level descriptions into executable detail—and makes the quality of the description, rather than the fluency of the generator, the central engineering problem.

Ground Truth. (2026, September 4). Program synthesis: making a computer write the program from the specification. Ground Truth. https://groundtruth.day/learn/program-synthesis.html

@misc{groundtruth:program-synthesis,
  title  = {Program synthesis: making a computer write the program from the specification},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {sep},
  url    = {https://groundtruth.day/learn/program-synthesis.html}
}

Topics: programming · specifications · verification · agents · fundamentals