I'm definitely interested in this! There are significant challenges here though, particularly with respect to combining dependent types with effects and coeffects! This is open research, but significant progress is being made, and I'm hopeful. I'm currently keeping an eye on https://github.com/granule-project/granule, which seems like it might have some interesting things to say about this.
Currently I'm trying to learn how to implement dependent types in my programming language, Pikelet: https://github.com/pikelet-lang/pikelet (currently doing a rebuild of the front-end in https://github.com/brendanzab/rust-nbe-for-mltt). I'm hoping that once I've done this I might eventually be able to start looking at implementing something to do with borrow checking in it, but who knows! The more I learn the less I seem to know! Always interested in chatting to people about this at our Gitter channel: https://gitter.im/pikelet-lang/Lobby
> Idris is perhaps the most famous dependently typed language.
I'd probably put Coq and Agda ahead of Idris in terms of being well known and established, but Idris is certainly pretty cool in how it tries to target practical programming.