HackerTube / Video
Type-Driven Development in Idris — Edwin Brady
Scala World
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.
HN points to it as a demonstration of type-directed editing with typed holes, which some see as a likely future of programming.
5 Hacker News mentions · 2019–2024