Programming by Navigation
summary
Defines Strong Completeness and Strong Soundness as showing all and only valid next edit steps, reduces synthesis to a type-inhabitation oracle, compiles types and semantic preconditions to Datalog via Curry‑Howard, and implements HoneyBee. HoneyBee uses the oracle to enumerate valid navigational steps, handles benchmarks with infinitely many solutions that enumerative baselines cannot represent, and outperforms two baseline variants on finite cases; artifacts and eval are provided.
AI-written summary · about
chapters (11)
- 0:00Programming by navigation intro
- 1:04Traditional synthesis limits
- 2:07Interactive synthesis pitfalls
- 3:29Strong completeness defined
- 6:36Component synthesis guarantees
- 11:06Type systems shortcomings
- 12:51Type inhabitation oracles
- 14:34Honeybee tool results
- 15:36Impossible guarantees
- 16:39Extending beyond type systems
- 17:28Q&A
related talks
20mAutomating the Design Recipe
13mProgramming with a Read-Eval-Synth Loop
32mTotally Live Programming with Hazel (Progress Report)
38mType System Foundations for Super-Charged Semantic Code Search
57mVariant analysis
29mType Inference Techniques: Implementation and Formalization, Better Together
16mDigging for Fold: Synthesis-Aided API Discovery for Haskell
24mA Counterexample-Guided Debugger for Non-Recursive Datalog