I guess since F* is similar to F# or ML you could have a pretty cohesive solver to production toolchain. Having OCaml as an output option is great too.

I was looking at Idris with the C backend as a way of formalizing my programming for production programming. This makes another set to evaluate before deciding. I realize they are quite different, but I am just experimenting at this moment.