'Dependently typed systems programming' was something that really excited me when I first learned of Idris, but it seems that they have backed down from that claim. Indeed, the home page now reads, "Idris is a general purpose pure functional programming language with dependent types".