> This means that everything specified with a dependent type must be deductively proven, or it has to be specified in some other way (i.e. you also need contracts), or else you risk making even your simple types unsound (although I hear some people are working on relaxing that problem, and that's what I mentioned in my previous comment). But properties differ greatly both in the confidence you need as well as the effort they require to achieve that confidence. Contracts give you the freedom to specify your program however you like, and then choose, for each property, which method you'd like to use to verify it -- deductive proofs, model checking, static analysis, concolic tests.
What practical distinction are you drawing here? Surely with any approach you either have a fully sound proof of a given proposition, or you have a potentially unsound proposition that you've tested at whatever level you feel appropriate. Like, if I have a SortedList type that can produce an assertion that, given n <= m, l[n] <= l[m], either the constructors of SortedList bake that in as a deductive proof, or they unsoundly assert it and I apply some level of static analysis and/or testing to them - how's that any different from what I'd do using any other technique?
> 4. Because dependent types are so tied to the program, the program must be written with the specific properties you want to verify in mind. If, after writing the program, you want to prove other properties about it, you'll probably need to rewrite it.
I'm not entirely convinced that this is any harder than any other approach - you'd have to propagate the new properties you were interested in through the code, sure, which would likely involve changing the types that the relevant points in the program were annotated with. But isn't it much the same process with a detached proof of the program property?