Types are a precious instrument to document our code and to catch errors at compile time, but they could be much more.
What if we could use types to drive our design process, to model precisely our domain and continuously receive feedback on it while we produce code? What if we could not only use types to find errors but also to actually prove the absence of errors?
If we introduce types as a first-class language construct, all of this, and much more, becomes possible.
In this talk we will see how to bring into play the full power of types using Idris, a purely functional programming language with dependent types, letting the types guide the development and being assisted by the compiler itself.