Idris is a new academic programming language with a dependent type system of unprecedented power. And, remarkably for an academic programming language, it's actually a general purpose language that you can use to write real programs as opposed to just proving theorems and publishing papers. It's what all the cool kids are talking about ("all the cool kids" is code for me) and it seems to be headed straight for world domination ("world domination" is code for more than 10 people), so I would like to give you a gentle and brief introduction to Idris and dependent types, and try to explain why they're so amazing, and afterwards maybe you'll want to join the Idris revolution as well (or maybe run away screaming which is fine too).