http://www.ats-lang.org/ i keep getting rewarded for never being satisfied with a programming language. will it end ??
ATS is the personal project of a single researcher starting with deCaml in 1999. ATS brings dependent types to systems programming by compiling to C with no runtime of its own. It's not quite as flexible as Idris, but it can compile to Arduino or anything else anything C can !!
explanation of dependent types: http://tojans.me/blog/2015/02/06/how-to-explain-dependent-typing/