Research Methods for Designing Next-Generation Programming Systems
summary
Claims a structure editor called Hazel makes every edit state syntactically, statically and dynamically well defined, with mechanized Agda proofs (a “cat sensibility” theorem) and a totality theorem for type-error marking. Builds a live-editor and Tyler gradual-structure-editing UI with live literals and sliders; classroom deployment with a few hundred students shows a five‑minute onboarding and productivity comparable to text editing and better than MPS on modification tasks. Warns agentic AI needs action languages and capability controls; small agent studies reach only double‑digit correctness on GitHub issues.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 13:22Live programming challenges
- 15:34Structure editing in Hazel
- 25:25Structure editing demo
- 31:08Evaluating user studies
- 39:23Live literals beyond code
- 47:53Live literals embedding demo
- 55:59AI assistance in programming
- 1:03:21Agentic AI challenges
- 1:14:26Planetary-scale live program vision
- 1:29:12Research methods and future
- 1:31:43Q&A
related talks
21mModifiable Software Systems: Smalltalk and HyperCard
21mMechanised Hypersafety Proofs about Structured Data
27mOperationalizing the Integration of User Interaction Specifications in Modeling Editor Synthesis
52mThink Abstractly, Work Concretely
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
28mWhat You See Is What It Does: A Structural Pattern for Legible Software
59mBetter Code: Human Interface
47mThe Meaning of LIVE