Edwin Brady - Idris 2 - Type-driven Development of Idris
In brief
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.