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

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?

• There has been some work done on this for Javascript. [linkhttp://goto.ucsd.edu/~ravi/research/oopsla12-djs.pdf) – jcarpenter2 Nov 28 '17 at 9:59
• Your link format is wrong. It should be like this: link to the paper – ice1000 Nov 29 '17 at 13:21

• It may be hard to interpret dependent types in the context of side effects. What does a value of type $x=y$ even mean if $x,y$ can change their values at runtime? Does this mean a term can be well typed at one point, and dynamically become ill typed? Or can you only use dependent types for immutable values?