With the version .99 release in December, Idris is pushing its way into being a complete language. It is purely functional with similarities to Haskell, and a type system like Agda but is aimed at more general-purpose use than solely academic. We’ll look at its syntax, how it functions, and along with this, we’ll compare it to other functional languages. Finally we’ll talk about how it’s designed to function with a Type Driven Development approach.