Edwin Brady just released a book titled "Type-Driven Development with Idris".
Here's a quote from the book:
[In Type-Driven Development] We put the type first, treating it as a plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete and working program which satisfies the type.
If we have a powerful Type System and a helpful Type Checker, we can start designing our program by defining its types. Then we start filling in the implementation, guided by the compiler.
There's also a concept of Holes. We can syntacticly define a part of the program that we don't know how to write. The compiler will infer types of holes, show it to us and help us fill them with implementation.
I'm curious about your thoughts. Did you try this approach already? Would you like to try it out?