Type-Driven Development in Idris with Edwin Brady

HN points to it as a demonstration of type-directed editing with typed holes, which some see as a likely future of programming.

Edwin Brady, creator of Idris, introduces type-driven development in a dependently typed language. He shows types being written first and programs derived with interactive editing, then extends beyond simple examples to programs that interact with users and networks.