#9 (downgrading mut refs to shared refs) is a big one. It makes things quite a bit more complicated in the context of our work on the OCaml-Rust interface (more precisely the safe interface for the GC). As I understand it, this is not a sacrifice we make at the "Altar of Memory Safety", but one we make at the Altar of Mutex::get_mut and Cell::get_mut, which is a much smaller altar (how often do you find yourself in possession precisely of a mutable borrow of a Mutex or of a Cell?).
Note that the approach in the original post is also wrong if the GC sees the expected value, because it would try to access it regardless of whether the prediction is valid.
This is about the classic trick of speculating on values using branch prediction (if value == expected then f(expected) else f(value)), which is always fun to see. But be careful in OCaml, as the memory model relies on the memory ordering of data dependencies (e.g. on Arm) to ensure memory-safety, so I suspect that this trick might be in general memory-unsafe in the presence of data races (more precisely values from other threads might be seen before their initialization). (OCaml memory-safety claims do not apply here because it uses Obj.magic.)
To clear up any misconception, out of the box OCaml will behave like OCaml 4 with a single domain and a "domain lock". Programs currently using multiple threads for concurrency will remain single-core for the time being, as they will need to opt-in to parallelism features. In this sense, adding parallelism to OCaml does not break existing programs, but they still might have to be audited for thread-safety depending on how they want to use parallelism. There is no magic.
The development of the OCaml-Rust interface is a bit organic. `ocaml-interop` aims to be a low-level but safe interface. At Inria we worked with the author to integrate ideas about using Rust's type system to safely work with a GC. We have more ideas to make it better; if someone wants to commit engineering time in this area they should feel encouraged to contact me.
Baker's paper is visionary in that it announces a link between linear logic and move semantics for resources more than a decade in advance. As we know this was put into practice by C++ and Rust. Compared to linear types, it amounts to operating a change of perspective from the quantitative interpretation (is it copied? is it dropped?) to a qualitative one (how is it copied? how is it dropped?). This is very much in spirit of linear logic (though it takes a bit of work to relate these ideas to Girard's mathematics). It answers questions that linear types were never able to, such as how to mix linearity and control. I take this paper as an example that there is more to linear logic than linear types!
As the paper clarifies, this is for the performance of non-atomic read/writes in sequential setting. The paper left the performance evaluation for atomic read/writes to future work. Is there any indication yet regarding the performance in a parallel setting compared to weaker guarantees?