[zokier]

Does anyone have experience using one of the more formal method oriented languages (e.g. Idris, Agda, F* etc) as their "daily driver" language, i.e. using them for general purpose programming, for any extended period?

I'm dreaming that by focusing on correctness one could reduce the maintenance churn that then can lead to various other spurious changes. But I don't know if any of those languages are really suitable to "real world" use, nor if they really provide such dramatic reduction of bugs that one would hope for.

[exdsq]

My colleagues use Agda but only for things like protocols or core features, Haskell is better for general purpose code

[nanagojo]

Idris is actually a general purpose language unlike the rest you listed.

[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