3 ms·
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 Pyth
by eggy 10y ago
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.
- ergl 10y agoYes, 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
- eggy 10y agoI 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.
- pron 10y agoZ3 (as well as other SMT solvers) is used by TLA+ (also MSR)