Dear members,
As far as I understand, ReScript cuts the ties with OCaml in order to be closer to JS.
OCaml belongs to an ecosystem of proven software, giving a lot of protection against bugs and its resulting security breaches.
If I got this correct, isn’t this change a weakening of the foundation of the language?
And if so, how is this weakening dealt with?
Regards,
Rainer
ReScript is using the OCaml type system and optimizes to a subset of OCaml’s semantics that compiles to a subset of JS. It will continue to compile OCaml source files (.ml) in the constraints of the OCaml version ReScript is built with. It never compiled to OCaml native, so it’s really hard to compare it to the native runtime characteristics.
The core ReScript language is strongly typed and runtime safe. IO, remote data and interop are as safe as you treat them in your programs. Which means if you write pure ReScript code w/o exception throwing code, you have the same type / runtime safety guarantees as in vanilla OCaml. That’s a sensible design that works really well in practise.
Please note that this design has never changed since the inception of the compiler (originally called BuckleScript) several years ago. The introduction of the ReScript brand never made it less safe, it’s literally the same compiler.
2 Likes
OCaml doesn’t give as much protection as you might think 
Check out this giant hole in a critical OCaml component of the Xen hypervisor (runs Amazon EC2 instances) that was missed purely due to human error: https://nvd.nist.gov/vuln/detail/CVE-2020-29479
Can you give a concrete example of a ReScript security issue, e.g. a CVE, that causes your concern?
Actually from the security point of view, it is better than native ocaml. Since the generated JS code can be audited for security concerns and JS runtime generally is running inside a sandbox.
2 Likes
Thank you for these answers.
My question is a bit ‘in theory’ from an intermediate trying to work as secure as possible.
Writing software is hard, more so if it aims to be secure. Having a theorem prover like Coq for instance is a big help, but offers no protection against reasoning errors.
What does help is having a concerted effort aiming for the best, each correcting the other.
In my mind working side-by-side with the Deepspec toolchain to reach a proven line from math to the browser and the underlying protocols is a distant, but worthy goal.
Of course, with any translation the results should be checked. No magic bullets available.
In this article how-i-switched-from-typescript-to-rescript the author states that ReScript is “a ReasonML which freed itself of the yoke of the OCaml ecosystem”. Well, part of the yoke is there for a reason, is my thinking.
So my concern is that ReScript may not get valuable feedback from the community of which OCaml is a part, thus weakening itself.
I think it’s better not to take things like ‘ReScript is freed from the yoke of the OCaml ecosystem’ too literally. But even if you do, it’s talking about the ecosystem, not the core OCaml compiler. Internally ReScript is still an OCaml compiler (or at least the major parts of it are).
The examples you cited–Coq and Deepspec–are not, as far as I know, big parts of the OCaml ecosystem in industrial applications like, say, webapps (which is ReScript’s focus). So I don’t see how they’re relevant here.
If you have any examples of specific feedback from the OCaml community that is missing and weakening ReScript, that would be interesting. But to be honest I don’t think there is anything like that. In fact I rather think it’s the other way round: ReScript (previously BuckleScript) users have discovered OCaml typechecking bugs that have been submitted and fixed upstream. If anything, I think upstream OCaml has majorly benefited from the thorough and wide-scale usage that ReScript gets.
1 Like
Even though Coq and Deepspec are not big parts of the ecosystem, they are central to my work. I can’t go where the OCaml compiler doesn’t go.
So that is the assurance I was hoping for.
Thank you.
Hi, such discussions are too high level that I am not sure if I follow you.
- I think what you are concerned is about correctness using theorem prover but not security
- Based on my understanding of Coq, it extracts Coq into OCaml source code which we also support,
so the Coq to browser PATH seems to still work
1 Like
If you couldn’t follow me, I am sure I had dropped the ball somewhere.
You are all very capable and professional here.
My angle is to also prove the protocols I am using. Then I would enhance my security, right?
To put it another way: can you give us an example of what you would do with the upstream OCaml compiler that you are unable to do with ReScript?
1 Like
I am developing an exchange protocol in Coq via the Disel framework. Server OCaml; client ReScript, thus keeping the codebase close together.