  We present a system called Smyth for program sketching in a typed functional
language whereby the concrete evaluation of ordinary assertions gives rise to
input-output examples, which are then used to guide the search to complete the
holes. The key innovation, called live bidirectional evaluation, propagates
examples "backward" through partially evaluated sketches. Live bidirectional
evaluation enables Smyth to (a) synthesize recursive functions without
trace-complete sets of examples and (b) specify and solve interdependent
synthesis goals. Eliminating the trace-completeness requirement resolves a
significant limitation faced by prior synthesis techniques when given partial
specifications in the form of input-output examples.
  To assess the practical implications of our techniques, we ran several
experiments on benchmarks used to evaluate Myth, a state-of-the-art
example-based synthesis tool. First, given expert examples (and no partial
implementations), we find that Smyth requires on average 66% of the number of
expert examples required by Myth. Second, we find that Smyth is robust to
randomly-generated examples, synthesizing many tasks with relatively few more
random examples than those provided by an expert. Third, we create a suite of
small sketching tasks by systematically employing a simple sketching strategy
to the Myth benchmarks; we find that user-provided sketches in Smyth often
further reduce the total specification burden (i.e. the combination of partial
implementations and examples). Lastly, we find that Leon and Synquid, two
state-of-the-art logic-based synthesis tools, fail to complete several tasks on
which Smyth succeeds.
