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.
The Python looks clean and familiar too.
F* the theorem-proving, program-verification language from MS is ML-like, and exports to OCaml and F#.
Can the Z3 SMT solver be used for F*'s SMT needs? I haven't found a link yet.