> There's pretty much no safety gain from using Rust over OCaml.
> But if you use OCaml you don't have to worry about borrow checking.
I've never written any OCaml, when you choose not "to worry about borrow checking" how does OCaml arrange to ensure your program is free from data races in concurrent code anyway? Or do you consider that "pretty much no safety gain" ?
OCaml's memory model specifies bounded space-time SC-DRF.
What this comes down to in simple terms is that data races have well specified semantics and their effects are bounded both in terms of what is affected by a data race, and when it's affected.
Using C as a starting point, a data race can modify any region of memory, not just the memory involved in the read/write, and the modification can be observed at any time, it might be observed after the write operation of the data race executes or it can be observed before the write operation executes (due to instruction reordering).
In Java, data races are well specified using bounded space SC-DRF. This means that unlike C, data races are NOT undefined behavior. A data race is limited to only modify the specific primitive value that was written to. However it does not specify bounded time, so when the modification of that primitive value is observed is not specified by the Java memory model, it could happen before or after the write operation.
OCaml's memory model specifies both bounded space and time SC-DRF. When a data race occurs, it can only modify the primitive value that was written to, and the modification must be observed no sooner than the beginning of the write operation and no later than the end of the write operation.
That was a very long-winded non-answer, but I think I understood it to be essentially "Yes".
I'm definitely not an expert, but to me this memory model sounds like a more circumspect attempt to carve out a set of benign data races which we believe are OK. Now, perhaps it will work this time, but on each previous occasion it has failed, exactly as illustrated by Java.
Indeed the Sivaramakrishnan slides I'm looking at about this are almost eerily reminiscent of the optimism for Java's memory model when I was younger (and more optimistic myself). We'll provide programmers with this new model, which is simpler to reason about, and so the problem will evaporate.
Some experts, some of the time, were able to correctly reason about both the old and new models, too many programmers too often got even the new model wrong.
So that leads me to think Rust made the right choice here. Let's have a compiler diagnostic (from the borrow checker) when a programmer tries to introduce a data race, rather than contort ourselves trying to come up with a model in which we can believe any races are benign and can't really have any consequences we haven't reasoned about.
Of course unsafe Rust might truly benefit from nicer models anyway, they could hardly be worse than the existing C++11 model but that's a different story.
> But if you use OCaml you don't have to worry about borrow checking.
I've never written any OCaml, when you choose not "to worry about borrow checking" how does OCaml arrange to ensure your program is free from data races in concurrent code anyway? Or do you consider that "pretty much no safety gain" ?