Idris is explicitly billed as a programming language. You can do pretty sophisticated programming in Coq too (Coq can be reasonably straightforwardly compiled down to Ocaml, Haskell and some other languages.)