[zokier]

Agda might be bit borderline, but any particular reason why you consider F* less general purpose than Idris? It's own intro says

> F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification

I haven't used either, so that's why I'm asking. Certainly going by their marketing F* seems very practical oriented, fusing common sensibilities from F# with formal methods