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. Most theorem proving languages are focused on mathematics or proving things about a program, and they are very abstract. This language appears to have a goal of bridging the gap and making it simple to write pr…
> 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?