Edwin Brady：Idris 2 的类型驱动开发

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.

Why HN likes it: Recommended as the best demo of interactive, compiler-assisted dependently typed programming in action.

“Watch Edwin Brady's demo of Idris 2 [2] to see this form of interactive development in action.”