Hi Joel, As long as your main interest is Web development, have you considered F*'s "father" - F# (https://fsharp.org)? In particular, WebSharper (http://websharper.com/) and Fable ( http://fable.io/)?
On the other hand, maybe the problem with polymorphic comparisons in OCaml might be solved with Modules and Functors? Best regards, *Alexander Tchitchigin* Software Developer *Positive Technologies* Tel.: +7 (495) 744-01-44 Fax: +7 (495) 744-01-87 E-mail: achichi...@ptsecurity.com www.ptsecurity.com On Fri, Dec 7, 2018 at 3:43 PM Joel Jacobson via fstar-club < fstar-club@lists.gforge.inria.fr> wrote: > 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 rewriting > the 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 >
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
