Barliman: trying the halting problem backwards, blindfolded
summary
Barliman is a prototype smart editor that completes programs from partial definitions and tests using a relational interpreter written in miniKanren EDSL (compatible with core.logic). It synthesizes concrete defs (concat, reverse with accumulator trick), generates a quine through layered evaluation, and checks/proves propositions with a proof checker. Some tasks fail (deep nested remove-foo, naive reverse) because search is exponential; heuristics and parallel runs are proposed. Implementation work yields huge speedups—claimed 10^7–10^8 faster over earlier demos—and the UI remains experimental.
AI-written summary · about
chapters (20)
- 0:00Intro
- 1:10Introducing Barliman 43
- 3:24Defining Concatenate
- 4:28CanCat
- 5:03Barliman
- 6:36Whats missing
- 8:12The hole
- 9:36Reduce right
- 10:50UI challenge
- 14:03Program synthesis
- 15:02Interactive IDE
- 16:28Synthesis
- 18:29Remove foo
- 21:47Lets have fun
- 22:43Getting it running
- 23:39eval
- 24:20scheme interpreter
- 25:40proof checker
- 27:04test
- 31:04conclusion
related talks
20mKanren Light
30mToward Programming Languages for Reasoning -- Humans, Symbolic Systems, and AI ...
47mLogic Programming à la Carte
53mSemantics-based program manipulation in the age of LLMs
33mHolbert: Reading, Writing, Proving and Learning in the Browser
40mminiKanren Philosophy
31mLetting users do the undecidable: lessons from program synthesis
32mDon’t Call Us, We’ll Call You