For me, C++ as its implementation language is one of the most promising things, as I suspect it's a significant reason why it's so much faster to check things than Idris. The speed difference is significant enough that I prefer it over Idris in spite of Idris' broader feature set: <1 second vs 10 seconds makes a huge difference to workflow when proving small lemmas (although it's possible I've somehow set up Idris wrong).