Program Sketching with Live Bidirectional Evaluation
summary
Smyth implements live bidirectional evaluation to run and unevaluate partial programs, turning assertions into per-hole constraints that are fed to Myth (used as a black box) so sketches and examples jointly guide synthesis. It synthesizes recursive functions without needing trace-complete example sets, completes 38 of 43 Myth benchmarks, and typically needs about 65% of expert examples Myth requires; with simple user sketches specification size drops to roughly 46%. The system emits concrete case splits, hole environments, and verified completed functions.
AI-written summary · about
chapters (7)
- 0:00Intro
- 0:21PROGRAM
- 2:49MYTH Limitation
- 4:58SMYTH
- 7:00LIVE UNEVALUATION
- 9:16TRACE COMPLETENESS
- 11:32EXPERIMENTS
related talks
13mProgramming with a Read-Eval-Synth Loop
28mScooPy: Enhancing Program Synthesis with Nested Example Specifications
14mLooPy: Interactive Program Synthesis with Control Structures
21mLive Verification in an Interactive Proof Assistant
25mLive Programming and Programming by Example: Better Together
20mEquivalence by Canonicalization for Synthesis-Backed Refactoring
17mAccelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
43mStop Writing Dead Programs