Dear F* hackers, I started learning OCaml a few months ago because I wanted a safer language than Javascript.To my disappointment, there are problems in OCaml with polymorphic comparison that seems hard to solve,so I continued my search for an even better language, and I found F* which looks promising. However, the ecosystem currently growing for OCaml thanks to ReasonML is really promising,and to me, interop with the Javascript world is important.
I would therefore like to continue writing code in OCaml, but I want to benefit from the increased confidence of security and correctness offered by F*. I've looked at the OCaml code generated by F*, and it looks really nice. My plan is to write as much code as possible in F*, convert it to OCaml, and write the integration code to interop with Javascript in a mix of OCaml and Javascript. Now to the question, Would it be imaginable to automatically identify fragments of OCaml code that could be "lifted" to F*? (I.e., the opposite of what the F* compiler currently does, OCaml -> F* instead of F* -> OCaml). This would be very useful in a situation when you have third-party OCaml code you want to use, such as any of the stdlibs (Batteries/Belt/Core), but you're afraid of using them because you don't fully trust or understand the code. If F* could tell you what OCaml code that could be translated to F* to prove security/correctness properties of the code,and what code that cannot be lifted for various reasons, the developer could then focus on analysing and rewritingthe problematic code that cannot be lifted. This way, a project could gradually increase the coverage of code that can be lifted to F*. It would be really interesting to hear your thoughts on this. Best regards, Joel Jakobsson
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
