HackerTube / Video
Edwin Brady - Idris 2 - Type-driven Development of Idris
Curry On!

Edwin Brady, creator of Idris, presents Idris 2 and demonstrates type-driven development, where the compiler assists by filling holes and suggesting implementations from types.
Recommended as the best demo of interactive, compiler-assisted dependently typed programming in action.
5 Hacker News mentions · 2019–2023