As an example this is Haskell's core language:
data Expr b
= Var Id
| Lit Literal
| App (Expr b) (Arg b)
| Lam b (Expr b)
| Let (Bind b) (Expr b)
| Case (Expr b) b Type [Alt b]
| Tick (Tickish Id) (Expr b)
| Type Type
| Cast (Expr b) Coercion
| Coercion Coercion
data Type
= TyVarTy Var
| LitTy TyLit
| AppTy Type Type
| ForAllTy !TyCoVarBinder Type
| FunTy Type Type
| TyConApp TyCon [KindOrType]
| CastTy Type KindCoercion
| CoercionTy Coercion
If you look closely you'll notice quite a lot of duplication between the two (see the first 4 and the last 2 constructors). Haskell is effectevily using the same language (lambda calculus) to describe types and expressions though with different syntax.And this is Lean core language (a dependently type language):
inductive expr
| var : nat → expr
| sort : level → expr
| const : name → list level → expr
| mvar : name → name → expr → expr
| local_const : name → name → binder_info → expr → expr
| app : expr → expr → expr
| lam : name → binder_info → expr → expr → expr
| pi : name → binder_info → expr → expr → expr
| elet : name → expr → expr → expr → expr
| macro : macro_def → list expr → expr
Imo dependent types provide a surprising answer to the question "What is the best type system?". Different languages have different type systems and as they evolve to become more expressive at a certain point they become Turing complete (e.g. C++, Typescript, Haskell, ..). So we end up with two separate languages - the language itself to describe programs and the type system to describe types.So what's the best type system? Dependent types' answer: the language itself. Instead of having two separate languages, have a single language that acts as its own type system, powerful enough to describe both programs and types. Then types become first class - you can pass them to a function as parameters, or return them as values, or use any function at compile time.
In physics progress usually comes in the form of unification. Two seemingly separate phenomena (say electricity and magnetism) turn out to be described by a single theory. Dependent types provide such a unification between expressions and types in programming languages. Imo definitely a step forward in the noisy sea of programming languages.
That's not even touching the mathematical side of things, Curry-Howard correspondence, proof assistants and using dependent types for proving theorems.