A talk about the wonderful world of types and programming languages, with a dash of formal verification. Does your programming language get you down? It probably should! Ever wish you could prove that your program was correct? Maybe you can! Join us as we briefly explore some alternatives with typed functional programming languages. With a bit of luck you will catch a glimpse into how programming languages can make your lives easier, and the world a better and safer place. Types aren't the Java-esk horrors of your nightmares, instead they can make programming a pure delight! Let's discover why that annoying person keeps talking about Haskell, and why that even more obnoxious person won't shut up about Idris.