Mind elaborate a bit more? The title sounds interesting, do you have to pick up another language in order to gain from the book?

The book is specifically written around the Idris language, so some aspects would not work in most other languages. If you are willing to accept the loss of tooling, you can apply the development practice but you lose a lot. With Idris, a partial program is still verifiable even if not executable. Compared to an incomplete C program.

A particular quality of Idris is the ability to leave "holes" in programs. That is, if I don't know what's going to happen in this function, I can leave a hole:

  main : IO ()
  main = putStrLn ?greeting

I can then extract that hole into a new function and develop its particular capabilities. This will type check. Idris understands that ?greeting must be a string (or something which will produce a string).

If you have some experience with Haskell or SML or OCaml, it's not too hard to pick up the language (particularly the first). It'll look and behave very similarly to what you've seen before. If you aren't familiar with them, you'll be learning a whole new language, but the book is a good introduction to the language and the concepts the language introduces.

> do you have to pick up another language in order to gain from the book?

No, there aren't any prerequisites going in. The book is basically a huge tutorial on Idris, functional programming, and dependent typing, so you'll be pretty fluent in Idris by the end of it. Also, Idris without dependent types is basically a cleaned up Haskell, so you'll be somewhat fluent in Haskell by the end of it too.

If you're asking, "I'll never use Idris after working through this book; is there still something to be gained wrt/ my day job in C++/Java/etc?"... I would say that some of the basic functional programming insights would carry over--immutability, higher order functions, separation of concerns, totality, etc.--but the dependent type stuff probably won't. Nonetheless, the parts that don't carry over (holes, type-level computation, etc.) are precisely the most eye-opening bits so at some level I have to recommend learning about them just for learning's sake.

> Mind [to] elaborate a bit more?

Sure, here are some of the "eye openers" for me:

- The biggest one honestly is that apparently it's quite possible to teach this stuff to ordinary mortals. I've had numerous false starts with Coq and Agda tutorials, but here I really appreciated that this is a very gentle, readable introduction to the topic. The book teaches dependent typing through "computery" examples, like programming a hangman console application, instead of "mathy" examples, like proving DeMorgan's laws. You can immediately appreciate how the techniques the book teaches you can be applied to normal, programming concerns: preventing resource leaks, reducing the need for writing tests, refactoring code to make it more generic, designing better APIs, etc.

- Central to the book, and book title, is this idea of "interactive development". The type checker becomes a kind of assistant that actually helps you design your code, not just this batch process at the end that slaps you on the wrist for forgetting a semicolon. This will be huge someday.

- I always thought that dependent types were something that you would only bother to spend the extra effort on for key parts of low-level, "hardcore" code; proving that a crypto function is secure, or that a particular concurrent data structure is deadlock-free... that kind of thing. This book completely turned that world-view upside down. Dependent types are more applicable to high-level "business logic" code; you can literally express (normally unwritten) business rules in types and have the computer mechanically check everything. Designing this stuff in dialogue with the typechecker can help you design better business rules.

- There are a bunch of mind-benders, like the type-safe printf function, that really challenge what you previously thought was possible. Gave me the same chills as when finally grokking other "big" ideas, like lisp's "code is data; data is code".

Great book. Maybe not practical in the short term but lots of amazing and eye opening concepts