Yes, and Idris actively encouraged iterative development that was based around its holes -- the book by Idris' creator Edwin Brady, Type-Driven Development[1],

Yes, and Idris actively encouraged iterative development that was based around its holes -- the book by Idris' creator Edwin Brady, Type-Driven Development[1], is an eye-opening introduction to this style of coding. [1] - https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...