Summary: Edwin Brady is the creator of the Idris programming language and Author of the book Type-Driven Development with Idris and a computer science lecturer. In this interview, we discuss dependent types, type holes, interactive and type-driven development, theorem provers, Curry–Howard correspondence, dependant haskell, total functional programming, British vs American spelling and much more.
