> The big problem I see with dependent types is that they ultimately require doing proofs... Proofs are hard, for those who haven't had the training and experience (the coding bootcamp goes right out), and proof software is bizarre, opaque, and normal manual proof techniques don't apply or are difficult to translate.

Proofs are programs (via curry-howard), so it's not completely unrelated to what programmers do day-to-day. Often, the correctness proof is as simple as beta-reduction, which languages like Idris will perform automatically; although this usually relies on a good choice of representation, which is a skill in itself. Outside of the happy-path, things certainly do get harder, but there's always a choice of whether to just skip the proof and say "trust me", which is no worse than other approaches.

A nice example is vector concatentation:

  // Peano encoding of natural numbers; e.g. 3 = Succ (Succ (Succ Zero))
  data Nat: Type where
    Zero: Nat
    Succ: Nat -> Nat

  // Addition, by recursing on the first argument
  plus: Nat -> Nat -> Nat
  plus Zero     y = y
  plus (Succ x) y = Succ (plus x y)

  // Lists of a known length
  data Vec: Nat -> Type -> Type where
    VNil : (t: Type) -> Vec Zero t
    VCons: (t: Type) -> (n: Nat) -> (head: t) -> (tail: Vec n t) -> Vec (Succ n) t

  // Append a Vec of length m to another of length n:
  //  - The resulting Vec has length 'plus m n'
  //  - All elements of the inputs and output have the same type t
  append: (t: Type) -> (m: Nat) -> (n: Nat) -> Vec m t -> Vec n t -> Vec (plus m n) t
  append _ _ _ (VNil _)         y = y
  append t _ n (VCons _ l x xs) y = VCons t (plus l n) x (append t l n xs y)

The correctness proof of 'append' follows from beta-reduction. In the `VNil` case, we need to prove that the type of y matches the return type, i.e. that for all n and t, Vec n t = Vec (plus m n) t.

In this branch the first vector argument is VNil _ (where '_' indicates something we don't care about). According to the definition of Vec, this argument has type 'Vec Zero _', and according to the type of 'append' it has type 'Vec m t'. Hence Vec Zero _ = Vec m t, telling us that m = Zero (and this occurrence of '_' corresponds to t, but we don't care).

Hence the context of this first branch contains the binding m = Zero; so our original equation Vec n t = Vec (plus m n) t beta-reduces to Vec n t = Vec (plus Zero n) t. This occurrence of 'plus' matches the first branch of its definition, so we can beta-reduce further to get 'Vec n t = Vec n t', Q.E.D.

In the second branch of 'append', we need to show that the type of 'VCons t (plus l n) x (append t l n xs y)' is the same as the return type 'Vec (plus m n) t'. First we can check that the recursive call to 'append' is well-typed, i.e. xs has type Vec l t, and y has type Vec n t, which are both correct.

The return type of that recursive call is Vec (plus l n) t, matching the '(plus l n)' argument given to 'VCons'. Hence the type of the 'VCons' call is Vec (Succ (plus l n)) t, so we need to match this with the overall return type of 'append': Vec (Succ (plus l n)) t = Vec (plus m n) t

In this branch, the first vector argument is VCons _ l x xs, which (from the definition of Vec) has type Vec (Succ l) t. According to the type of 'append', it also has type Vec m t, so we know that Vec (Succ l) t = Vec m t, and hence m = Succ l.

Hence our equation for the return type beta-reduces to Vec (Succ (plus l n)) t = Vec (plus (Succ l) n) t. The occurrence of 'plus' on the right-hand-side matches the second branch of its definition, so we can beta-reduce this to: Vec (Succ (plus l n)) t = Vec (Succ (plus l n)) t. Q.E.D.

The steps above correspond exactly to "running the program" (i.e. evaluating/reducing the expressions), and is performed automatically in languages like Idris. Hence we don't need to write out any separate "proof", the definition of the 'append' function is proven correct just by evaluating the expressions which occur in its types (taking into account the context of the branches those expressions occur in). This is the "happy path".

The reason I like this is example is that we can completely break it, simply by swapping around the 'plus m n' to 'plus n m' in the type of 'append'. That gives us expressions like 'plus n Zero' and 'plus n (Succ l)', which don't match the branches of 'plus', and hence won't beta-reduce. In order to make this work, we need to prove the general theorem 'plus x y = plus y x', and use that to flip the type into the original order. Proving that theorem requires proving lemmas like 'plus x 0 = x', etc. which is absolutely the sort of thing day-to-day programmers don't want to bother with!

On the other hand, it's certainly nice for library developers to have the option of proving such things. Again, we can always skip the proof if we don't feel it's worth the effort, and the result is no less safe than the non-dependent systems already used by those day-to-day programmers!