Idris 2: Type-Driven Development with the Compiler
Curry On! · Talk · 41 min · 2019 · YouTube title: Edwin Brady - Idris 2 - Type-driven Development of Idris
Why it's here
Recommended as the best demo of interactive, compiler-assisted dependently typed programming in action.
What it covers
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.