I think Idris (https://www.idris-lang.org/ https://www.idris-lang.org/) is primarily focused on using dependent types for programming, and even Lean has been ex

I think Idris (https://www.idris-lang.org/ https://www.idris-lang.org/) is primarily focused on using dependent types for programming, and even Lean has been expanding in this direction (cf. the Functional Programming in Lean book, https://lean-lang.org/functional_programming_in_lean/ https://lean-lang.org/functional_programming_in_lean/).