I like the Lisp/Scheme syntax better, but that is because I have studied Lisps far longer than Python, and I just find them easier for phrasing logic.

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.

Yes, afaik F* uses Z3 internally.

I don't have any links, but I know a guy working on formalizing the translation from F* to Z3

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.

Z3 (as well as other SMT solvers) is used by TLA+ (also MSR)

And an amazing example of why operator overloading is not the evil that people make it out to be.

I don't know why you've been downvoted. The interface does look neat. They did a good job with it.

Other example of such thing is Numberjack -- a constraint solve with multiple backends:

http://numberjack.ucc.ie/

Here is a send-more-money example solved in it:

http://numberjack.ucc.ie/examples/sendmoremoney

Sudoku:

https://github.com/eomahony/Numberjack/blob/master/examples/...