HackerTube.dev

"Type-Driven Program Synthesis" by Nadia Polikarpova

Strange Loop Conference · 14.7K views · 2018-10-16 · 39:40

Open on YouTube ↗

If playback is restricted in your region, try opening the original video. Use Mark watched to add it to your marked videos.

Overview

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.

On Hacker News

HN points to it as a motivating introduction to what program synthesis is and what types can do for it.

Recommended by 2 HN people across 2 months · HN mentions 2018–2024

Topics

Search by tags

What people said

ddellacosta · 2024-03 · Recommendation

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 [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]

Read the original HN comment ↗
agentultra · 2019-03 · Recommendation

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: [VIDEO] [0] [LINK] [1] [LINK] [2] [LINK] [3] [LINK]

Read the original HN comment ↗
kilburn · 2021-06 · Reference

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] [VIDEO]

Read the original HN comment ↗

Sources

Video by Strange Loop Conference, played through YouTube.

Data and selection notes

HN summaries and labels may contain AI errors. HN dates refer to discussions, not video publication.

HN Library: HackerTube export (2026-10-31) and open-index/hacker-news. Upstream summaries and classifications may contain AI errors.

Views, duration and playback status refresh separately from the published catalog. When an update fails, existing data remains visible.

Selection checks
  • SaaS & AI candidates: Topic keywords do not match
  • Editor-approved picks: Editorial review is required

Rule matches identify candidates. They do not guarantee video quality or financial results.

About the library and its sources