Can we add dependent type into an existing imperative programming language?

Question

As we know, dependent type allows programmers to write bugless programs.
But as I know there's only very few languages support dependent type, like Haskell with extensions, Idris, Agda, F*, etc.

Since these are all functional languages, is there any possibility to add dependent type into an imperative language?

I've googled and found some papers like http://www.ats-lang.org/MYDATA/Xanadu-lics00.pdf or https://www.cs.bu.edu/~hwxi/academic/papers/XanaduAbs.ps, but they create their own languages.