Thank you for the detailed response!
There is no doubt that any proof system is probably too expensive for use in the industry, both because of the correctness requirements that are somewhat relaxed and because the systems tend to be more complicated than idealized algorithms. I was just interested in the more theoretical mathematical implications of the dependent-type vs set-theory approaches, just out of intellectual curiosity (now that I've started using TLA+, I'm interested in other approaches).
In any case, going on a tangent, I was surprised to read your mention of an incomplete symbolic model checker. After growing to enjoy TLA+ so much, that was the first thing that I thought would be a great addition, as it would allow checking of different kinds of specs, like sorting algorithms (a very interesting bug -- which only occurs on very large arrays -- was found in Java's sorting algorithm using the KeY project for symbolic execution) and order-dependent data structures like B-trees, where small models are ineffective. Any more information on this effort? It's the first time I hear of it. I would imagine that given TLA+'s simple and clear semantics, implementing symbolic execution would be easier than for something like Java.
Ron