2 HN users recommended this talk2 months2018–2024score 2
Years with an HN recommendation, 2007–2026
HN points to it as a motivating introduction to what program synthesis is and what types can do for it.
Nadia Polikarpova's Strange Loop talk on program synthesis driven by refinement types, as in Synquid. It shows how rich type specifications can be turned into verified, executable code.
“for a motivating talk and explanation on what program synthesis is try this one” (HN, 2019)
For an introduction and motivation to TLA+ I recommend Hillel Wayne's talk Everything About Distributed Systems is Terrible [0] and basically anything he has written on his blog about the TLA+. I think following along with the TLA+ video course is really thorough and digestible once you've decided that you want to learn more [1]. You'll find the TLA+ Hyperbook is a useful reference and guide as you start specifying your own systems [2]. It has a number of examples and projects to work on. Eventually if you want to go deep after you've decided it's worth it for yourself, get into Specifying Systems the text book and bible of TLA+ [3]. Program Synthesis has a lot of research in it and is starting to show promising results. I'd say that while the research has been going on for a long time it's still rather new to industrial use... for a motivating talk and explanation on what program synthesis is try this one: [this video] [0] [link] [1] [link] [2] [link] [3] [link]
Motivating introduction to what program synthesis is
Oh yeah, you just reminded me of this cool talk I saw at Strange Loop a while back. Not about the AI parts but re: program synthesis in Haskell: "Type-Driven Program Synthesis" by Nadia Polikarpova [this video] Links to more projects and papers by Prof. Polikarpova: [link] I think this is one of the main projects she discusses in the talk: [link] EDIT: meant to mention this too, which I think has been around a bit longer, not that I've ever used it in production: [link]
> Good specifications are often written at a level that generating executable code from them is often undecidable and almost always intractable in practice. What about modern dependently-typed meta languages like Idris and program synthesizers like Nadia Polikarpova's work on Synquid? Type-Driven Program Synthesis, by Nadia Polikarpova (StrangeLoop 2018) [video] [this video] MIT Comcom: Synquid program synthesizer, and more command-line tools for the web [link] Idris Software Foundations [link]
Talk on synthesizing programs from refinement types (Synquid)
This is an active field of research. Search for "program synthesis". We are advancing, but the current state is... not mind-blowing yet (albeit somewhat cool!). See [1] for an example interactive demo and [2] for the corresponding presentation. [1] [link] [2] [this video]
Presentation accompanying an interactive program synthesis demo
Video list and Hacker News comment labels from HackerTube (prompted by @karpathy), released under ODC-By 1.0, built on the open-index/hacker-news archive. Hacker News data is provided by Y Combinator; comments remain the work of their authors. Video titles, channel names and thumbnails belong to their creators and are shown via YouTube. HackerTube Watch is an unofficial edition. Data export of 2026-10-31.
Plays via YouTube's privacy-enhanced embed
4 Hacker News comments
From the HN archive; up to 20 kept per video, favoring different commenters. Recommendations first.
Read more
Citations, criticism and jokes