Re: [fstar-club] OCaml -> F*
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
[fstar-club] OCaml -> F*
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
Re: [fstar-club] OCaml -> F*
On Fri, Dec 7, 2018, at 5:03 AM, Alexander Tchitchigin wrote: > 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? Yes, I've looked at F#, but I really want to use F*, it has many cool concepts that I want to benefit from, such as inferred type-and-effects and the use of Z3 to prove things about your code. I'm curious to know if there are any plans to help developers semi-automatically convert code fragments from OCaml to F*? ___ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
Re: [fstar-club] OCaml -> F*
Unfortunately, Refinement Types as all other types are only useful as long as you write them and prove (explicitly or implicitly) your code respect them. That's not the case for external code in libraries and frameworks, in your case for OCaml and JS code you have to interface with. You can declaratively ascribe (`assume`) types to external functions but you have no guarantees these functions obey to ascribed types especially when you update your dependencies. And even then you're very likely to suffer from information loss due to underspecification of external types, especially when your data or functions get passed through external functions and back. Even built-in `map` function in F* looses type information about function and data given to it. So overall your code is going to be only as good as OCaml/ReasonML types. Basically on par with F#. That's why it makes little sense to automatically convert OCaml to F* - you're not going to get the most important part, more precise Refinement Types as OCaml types lack them and you're unlikely to recover much even fully analyzing the source code. At least that's what my very limited experience tells me. :) 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 4:18 PM Joel Jacobson wrote: > On Fri, Dec 7, 2018, at 5:03 AM, Alexander Tchitchigin wrote: > > 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? > > > Yes, I've looked at F#, but I really want to use F*, it has many cool > concepts that I want to benefit from, such as inferred type-and-effects and > the use of Z3 to prove things about your code. I'm curious to know if there > are any plans to help developers semi-automatically convert code fragments > from OCaml to F*? > > ___ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
