Type-Driven Development with IdrisProgramming languages that support dependent types provide us with an expressive environment in which we can specify and reason about properties of our software programs.Type-Driven Development with Idris is an introductory text to dependently typed programming using the Idris programming language, which the book introduces, and to how we can use Idris' support for first-class dependent types to engineer software programs that are not only maintainable but programs that can also be formally verified.Type-Driven Development with Idris is not the first book to describe how dependent types are used to reason about software programs (Chlipala, 2013;Stump, 2016).While these books provide extensive coverage of the subject matter, they are aimed toward the theorists (squigglers) who wish to develop theories using dedicated theorem provers.What is nice about the book, and the Idris language, is that it is aimed more at engineers (bodgers) not used to squiggling or functional programming.Importantly, the book does not shy away from more squiggly topics such as totality, decidability, and theorem proving (which are required components for verifying programs) and introduces them at a gentle pace comfortable for the novice.The book is divided into three parts.Part 1 offers a general introduction to the basics of functional programming in Idris that is reminiscent of Hutton's Programming in Haskell (Hutton, 2016).The author considers the expected readers' background and ensures that those experienced enough can jump ahead where appropriate, and that those not so experienced are given the time required to learn functional programming in Idris.What is nice here is that the author, using the classic "Lists with Length" example, shows the need for types and how type-driven development helps with the software engineering process before the Idris language is introduced-thus, allowing one to gain an intuition for why type-driven development matters.Part 2 delves into the core of programming with dependent types in Idris, introducing language features and idioms that allow one to specify and reason more precisely about one's software programs than we can when using existing general-purpose programming languages.Specifically, the author introduces the reader to dependent types and how they can be used to write interactive programs and demonstrates how to verify these same interactive programs by using dependent types to reason, at the type level, about the structure of data and how dependent types can change how we view data to extend pattern matching in interesting and practical ways.Importantly, the book demonstrates how these idiomatic constructs support the construction of efficient verified code, an important aspect when one is developing real programs.The author makes backwards references, refinements, and extensions toward the examples mentioned in Part 1, giving the reader a chance to see previously seen concepts in action.More so, the running examples of a "word guessing

@article{Muijnck-Hughes20,
  title = {Type-Driven Development with Idris},
  author = {JAN DE MUIJNCK-HUGHES},
  journal = {Journal of Functional Programming},
  volume = {30},
  year = {2020},
  doi = {10.1017/s0956796820000143}
}