DT is definitely heavy-duty. There are massive unsolved problems about how to make, say, proof management... basically even possible. This is part of what make

DT is definitely heavy-duty. There are massive unsolved problems about how to make, say, proof management... basically even possible. This is part of what makes HoTT exciting, I believe, as it provides a formalized way of passing proofs and operations around over different types so long as there's a suitable homotopy. So while Idris is a very exciting research direction, it's completely fair to state that they have a hefty set of barriers to overcome before they truly demonstrate the value of DT in some larger variety of usecases besides just theorem proving.