> The thing about typechecking, though, is that you're essentially specifying your program's behavior twice: Once very detailed in the actual code and once at usually some lesser detail in the types.
How so? The implementation is not the specification; but the type is the specification. Like people like to say, the type is a Theorem, and the implementation is is the Proof of the Theorem. (In a very real sense.) And don't you need both?
Hopefully there can be some type inference at a certain scope, to avoid cluttering the code with a lot of 'obvious' type declarations. I forget exactly how dependently typed languages work in that regard right now (there certainly can't be full type inference).
> All the compiler does is checking that these two specifications are consistent with each other.
"All". That's already better than informal mathematical proofs.
> Your types can have bugs too, in which case nothing will help you.
Yes, just like any other kind of alternative specification there is. Short of mind reading, there is no getting around actually describing what we want. But where there is a distinction to be made is in what kind of specification is easy and declarative enough to use as to give the least likelihood of introducing bugs in the spec itself.
> What frustrates me about detailed type systems is that as detail increases, difficulty of writing the types will increase and type bugs will become more common.
I guess if we assume that we have collapsed/unified the type and term(/value) level, we can use any old Good Software Engineering Practice when it comes to keeping the types tidy. Like using type functions to encapsulate some of the detail: maybe have a `sorted(list)` function instead of having to write it out each time we need it.
This is just a guess though; I don't know how the dependent programmers do it. Well most of what I'm writing here is guessing, on some level.
(And judging by the pride that some people show when they proclaim that "half of our code base consists of just tests", well... I certainly think that types can be more succinct than that!)
> Now, assuming the bugs in your code and types are statistically independent that would still save you a lot of bugs, but I suspect they are not.
I guess if we go with the previous assumptions of a unified value/term level, then the statistical chances are the same in that types are just ordinary values, instead of the types belonging to its own language. ;) Then we just have to make sure that the amount of types is substantially smaller than the amount of "regular ol' code".
Typer er fremtiden. Håper jeg (kanskje).