‘Dependent types’ appear to add another layer of code or description, to verify the normal code. But is the word ‘verify’ sneaking in to mislead us? Looking closer, verification is not quite really what it does. It just adds more detail to the normal code, it just enriches the normal code's definitions of its abstractions. This is still a good thing: in fact, it is the best thing to do (but not really for typing reasons exactly, but for sofware engineering generally – more clarity is better).
Typing is in essence wholly ‘internal’. It is about relations within code: it is about consistency. Typing is not verifying against other information. In the terms of logic, it is not checking soundness, but validity.
That typing is about consistency is what makes it possible to do automatically. Otherwise ‘dependent types’ would lead to an unsatisfiable regress: you verify the code, but only with more code – so what verifies that code? another layer of verification? No amount of recursion will ever lead where verification really needs to go: external (human) judgement.
Consistency is about meaning the same thing, verification is about meaning the correct thing. In a way it is only a small, pedantic, supplementary point, but then again maybe it also captures something notable . . .