I thought I understood dependent typing (DT) properly, but the answer to this question: https://cstheory.stackexchange.com/questions/30651/why-was-there-a-need-for-martin-l%C3%B6f-to-create-intuitionistic-type-theory has had me thinking otherwise.
After reading up on DT and trying to understand what they are, I'm trying to wonder, what do we gain by this notion of DTs? They seem to be more flexible and powerful than simply typed lambda calculus (STLC), although I can't understand "how/why" exactly.
What is that we can do with DTs that cannot be done with STLC? Seems like adding DTs makes the theory more complicated, but what's the benefit?
From the answer to the above question:
Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from propositional to first-order logic.
This seems to make sense at some level, but I'm still unable to grasp the big-picture of "how/why"? Maybe an example explicitly show this extension of the C-H correspondence to FO logic could help hit the point home in understanding what is the big deal with DTs? I'm not sure I comprehend this as well I ought to.