tldr of https://serokell.io/blog/2018/12/17/why-dependent-haskell
He basically wants a language with a type system that lets you ensure that reading an element at an arbitrary position is safe and cannot crash because the index is always within the range of the array. He goes through all the mainstream languages and finds out that none would work.
He gives an example of a language that has this property, Agda. It's actually not a traditional language but a proof assistant. The way lookup is defined is the following way: