Edwin Brady – Idris 2: Type-Driven Development of Idris – Code Mesh LDN 18

I'm really a fan of the type-driven development process Edwin shows of here.

Especially the part where it can generate the correct matrix transposition logic as soon as it's been told that 'matrix' can only be used once. Very impressive.

I really hope at least some of that catches the interest of mainstream language designers/communities.