Lovely talk on type driven development in Idris 2, largely a live demo! https://youtu.be/mOtKD7ml0NU