DT is a hot topic in the PL community recently. It massively enhances the capability of a type system by turning it into a comprehensive logic system, so you can encode whatever properties you'd like to enforce into a type signature. Theorem provers have been taking advantage of the Curry-Howard correspondence for some time, but the implication of DT on real-world programming is still not well understood (we need more real-world projects written in DT languages). There are also ambitious projects that want to bring DT into the mainstream.
If you are interested, you can take a look at Lean [1], Idris [2], and a few others [3,4]. Often these languages have esoteric syntax, but there are projects using a more conventional syntax, too, e.g. Cicada [5]. "The Little Typer" [6] is a pretty good introduction to this topic.
[1] https://leanprover.github.io [2] https://www.idris-lang.org [3] https://github.com/agda/agda [4] https://coq.inria.fr [5] https://cicada-lang.org [6] https://mitpress.mit.edu/books/little-typer