> I studied formal languages for ~2 years and have professional experience programming coq. The real benefit of this language, over other formal languages is the focus on being able to write real programs in it.

How does Idris compare these days?