Smyth is a program synthesizer that will fill in "holes" in a program in a typed, functional language (approximately Elm in our formulation) when given input-output examples, or, more generally, arbitrary assertions about the behavior of the code. These assertions are just "normal code" and can serve as unit tests once the synthesis has completed.
Evaluation of these assertions internally gives rise to input-output examples which, along with the types in the program, guide the synthesis search to fill in the holes. The key technical innovation, live bidirectional evaluation, propagates examples "backward" through partially evaluated sketches (that is, programs with holes).
Live bidirectional evaluation enables Smyth not only to specify and solve interdependent synthesis goals over holes at arbitrary locations in the program, it also removes the need to specify "trace-complete" sets of examples recursive functions (that is, sets of examples that mirror the intended recursive behavior of the function to be synthesized), a major limitation of prior work on evaluator-based synthesis.
The name "Smyth" is a portmanteau of "sketching" and "Myth" (the type-and-example directed program synthesizer upon which the theory of Smyth is based). It was coined by Robert Rand who, incidentally, also coined the name "Myth."
A formal exposition of the system (including its evaluation and underlying theory) can be found in our ICFP 2020 publication, Program Sketching with Live Bidirectional Evaluation.
A non-academic introduction to the Smyth project can be found on the project webpage.
Code documentation for the system can be found here. The documentation for the core synthesis algorithm as outlined in our ICFP 2020 publication specifically can be found in the smyth/Smyth/ subdirectory. The codebase section below gives a high-level overview of the system.
Further details about the implementation of Smyth can be found in Justin Lubin's undergraduate thesis, Forging Smyth: The Implementation of Program Sketching with Live Bidirectional Evaluation.
opam, the OCaml package manager.
Install OCaml 4.08.1 with the flambda optimizer by running
opam switch create 4.08.1+flambda. OCaml versions after 4.08.1 should work fine too, but are untested.
make depsin the root directory of this project to download all the necessary
maketo build the Smyth executable. The executable is accessible via the
smythsymlink in the root directory of this project.
To replicate the experiments we have run to evaluate Smyth, you will also need the following tools installed:
- GNU Octave
- Python 2.7
- Python 3
To modify the documentation, you will also need the following tools installed:
- BeautifulSoup 4
The benchmark sketches from the experimental evaluation of Smyth are stored in
suites/SUITE_NAME/sketches and the input-examples used for those sketches are
suites/SUITE_NAME/examples. If you want to see the actual
synthesis output on just one of these sketches, you can use the
script that we have provided in the root directory of this project as follows:
./forge <top1|top1r|top3> <suite-name> <sketch-name>
So, for example, you could run
./forge top1 no-sketch list_sorted_insert
to see the top result of running the
list_sorted_insert benchmark from the
August 20, 2020: A new release,
icfp-2020-v1 includes module-level
documentation for the
smyth library and fixes a bug that caused
Experiments 2b and 3b to fail to run.
Running the Experimental Evaluation
Quick summary: navigate to
./run-all 10, look at
To run all the data collection and analysis for Smyth as described in our ICFP
paper, navigate to the
experiments/ directory and run the script
which takes a positive integer
N as an argument that indicates how many trials
per example-set size to run for each benchmark in Experiment 2b and 3b (the
We ran these experiments with
N = 50 (that is,
./run-all 50), which takes
about 2 to 2.5 hours to run on a Mid 2012 MacBook Pro with a 2.5 GHz Intel Core
i5 CPU and 16 GB of RAM.
If you would prefer to get the results faster (with the loss of statistical
precision), we would recommend running the experiments with
N = 10 (that is,
./run-all 10), which takes about 30 minutes to run on the same MacBook.
Once this script is complete, you can take a look at the results with any
phenomena of note explained in
Note: Rarely, due to timing issues with the UNIX Timer API, one of the benchmarks that is not indicated as a failure might crash with a "Timeout" exception during Experiments 2b and 3b. Even more rarely, a stack overflow error might occur. To combat these situations, the Experiment 2b and 3b scripts automatically retry a benchmark on unexpected failure.
lib/smyth directory contains all the code for the core
implementation of the Smyth synthesis algorithm. The
lib/stdlib2 directory contains helper functions that are used
throughout the codebase. The
src/ directory contains the code relevant
to the command-line interface to Smyth, as well as some code that is used for
its experimental evaluation.
The following table provides a roadmap of where each concept/figure in the paper can be found in the codebase, in order of presentation in the paper.
|Syntax of Core Smyth||
|Live bidirectional example checking||
|Assertion satisfaction and simplification||
|Type-and-example-directed hole synthesis||
|Type-directed guessing (term generation)||
To see how these concepts all fit together with actual code, you can take a look
at the "synthesis pipeline" in