Examples of Easy Dependently Typed Programming (in Idris)

Dependently typed programming is a green field. I want to present my experiences with Idris and how dependent types would fit into everyday programming, where proofs are not relevant but software correctness is still essential. I think dependently typed programming is not only for proof engineering.