You really don't need dependent types to do the printf thing, any language with GADTs or equivalent typing functionality can do it, see for instance OCaml's Pri

You really don't need dependent types to do the printf thing, any language with GADTs or equivalent typing functionality can do it, see for instance OCaml's Printf module. Although you do need a little bit of magic from the compiler to get that exact syntax, which you can get rid of with dependent types.