I viewed Leslie's interview in the Computer History Museum(1)(2) and at page 21 he explains the merits of abstraction and why it simplifies things compared to programming languages like Java that are very complicated. I could use the same arguments for dependent types.
Of course, in page 13, there is an example that shows that types are not useful, that I do not understand. In agda, one form of equality is between terms of the same type. And we need to prove that equality theorems so as to prove that a term has the correct type in an _expression_.
I do not understand why this is bad.
(Apart from that , I have quite a lot of reading to do about the history of TLA+ and why previous versions were not good.
1. Systems that only used temporal logic : What made them so complicated.
2. Separation into state machines for safety properties and temporal logic for liveness.
3. State predicates in temporal logic instead of actions.
4. .... and possibly more.
)