OK, I think I see where you're coming from. I don't think the distinction you make is a useful one. > A concrete difference would be, in dependently-typed lang

OK, I think I see where you're coming from. I don't think the distinction you make is a useful one. > A concrete difference would be, in dependently-typed language, you define a list type as [...] Coq is a dependently typed language, and while it has a definition like this for some thing (called vector, maybe? I forget), the definition for lists in the standard library is not dependent, and length is a separate function. You can still write a function like Fixpoint lookup (xs: list a) (idx: {n: nat | n < length xs}): a := ... I don't know how much experience you have with dependently typed languages, but it looks like you might have misunderstood tutorials showing that one can define a dependent list type as saying that one must define lists dependently? > And then the type checker/SMT solver will treat `length` as an uninterpreted function that always maps the same array to the same integer, and use it to prove things. Treating it as uninterpreted is quite weak. It allows you to prove simple callers of the lookup function, but not the implementation. Also, you would not be able to prove something like this: if idx < length xs then lookup (Cons foo xs) (idx + 1) else ... This is admittedly a silly example, but it should be provable. But you can only do that if you can reason about the relationship between length and Cons. As for automating proofs, I very very much agree that we need a lot more automation. But if that means crippling our theories to an extend that they are no longer expressive enough to verify our software, not much is won.