4 ms·
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
by ergl 10y ago
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
- 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.