Damn, this area of programming sounds very interesting, but I'm so so lost in these type compositions... Is it this Idris video you are talking about? https://y

Damn, this area of programming sounds very interesting, but I'm so so lost in these type compositions... Is it this Idris video you are talking about? https://youtu.be/X36ye-1x_HQ?t=1716 https://youtu.be/X36ye-1x_HQ?t=1716 I'm already having troubles following it after 8 lines of type definitions, while matrix transposition in the language of my choice is just `#(apply mapv vector %)` Sorry, I'm not trying to be dismissive, I just want the ergonomics of expressing my intentions to the computer be free of all this boilerplate while leaving compiler a possibility to give me some useful feedback when something might be wrong, are we really not there yet or are there languages aiming to make dependent types practical? You mentioned Coq, but I'm still not being able to find any code examples or some getting started guide in its official documentation...