Idris 2: Type-driven development of Idris

We've had lots of fun over the last couple of years investigating the possibilities and limitations of type-driven development in Idris. 

As we write larger programs, though, we're finding the implementation of Idris is showing the strain - such is the nature of "research quality software." Edwin recently decided the time was right to start again and implement Idris 2 in Idris. 

In this talk, Edwin will give an introduction to type-driven development (in Idris 2) and report on progress so far, showing off the most interesting features which the new design enables (notably, linear types and better type inference).