Even if a particular application doesn't require any multicore support, usually at work I won't be working on just one application as part of a project, there'll be multiple applications involved, at least some of which will require shared memory parallelism. To me it doesn't make sense to pick a language that can only be used for a few applications not all, as this leads to unnecessary duplication in library code and the like compared to just using one language (in my case, C++) for all of them (similar to how people prefer to use the same language for frontend and backend to reduce duplication). Especially when the lack of multicore doesn't bring any compelling advantages: it saves a few percentage points of single-threaded performance at the expense of completely ruling out most use-cases that require shared memory parallelism (or at least rules out any ways of doing them that aren't incredibly un-ergonomic), which seems like an absolutely terrible trade-off to me.
Here's a concrete example: comparing the Isabelle proof assistant, written in PolyML (a multi-core supporting SML implementation developed mostly by one guy) with Coq (which is written in OCaml). Interactive theorem proving in the former is a lot nicer as it takes advantage of multithreading not only for faster concurrent processing of proofs, but also to do things like running Quickcheck and Nitpick in a separate thread automatically to identify trivially falsifiable lemmas, and automatically finding stdlib lemmas that exactly solve a particular proof.
I think PolyML demonstrates that a lack of manpower isn't what stopped OCaml implementing multithreading support. Over the years there have actually been a few proposals/branches implementing some form of support, but all were rejected/abandoned. There was even one that just made the runtime reentrant (passing the runtime around directly instead of having it as a global variable), meaning the OCaml runtime could now be stopped and restarted when embedded in another application (e.g. C calling OCaml), a feature already present in Haskell, but this relatively simple improvement was also rejected (which personally bothers me a lot on a subjective level as I hate globals so it seems like a worthy improvement for its own sake). I remember waiting excitedly four or five years ago for it to be merged, a small but significant step on the path to multicore support, only for that hope to fade away as contributions to the branch slowed to a trickle then dried up completely. Without such extreme focus on avoiding decreases in single-core performance, it would have been much easier for a change like this to have been merged.
I think in recent times there is even less justification for rejecting multicore for affecting single-threaded performance. For two reasons: firstly, the recent addition of FLambda has brought performance improvements in many cases of over 10%, easily enough to compensate for any loss from multi-threading. Secondly, HFT now basically requires FPGA to compete, so single-threaded performance would presumably be of less concern to Jane Street (OCaml's biggest industrial user) now as they really shouldn't be using a software execution engine anyway (disclaimer: I say that as someone working at a competing HFT firm). And if Jane Street isn't doing HFT, then a drop of a few percentage points in single-threaded performance shouldn't affect them much anyway.
Finally, OCaml could always do what Haskell did and add a flag to toggle whether or not multi-threading is enabled, allowing single-threaded users to avoid any performance regression.
> things like running Quickcheck and Nitpick in a separate thread
In my experience with Isabelle, these tools provide feedback on the order of seconds (because they do expensive things). Maybe several hundreds of milliseconds, for simple cases. At these scales, it makes no noticeable difference what kind of parallelism solution you use. Spawning separate processes and sending messages would work just as well.
So the reason there is no parallel Quickcheck for Coq is more likely due to the fact that there is no Quickcheck for Coq, period.
One can have the kind of unsafe shared memory like C++ in OCaml by using a library like netmulticore. But the OCaml formalised memory model is offering the same kind of OCaml safety in multicore programs.
For your first point I'm not an advocate of using a single programming language for all kinds of things. But it's just my opinion.
Here's a concrete example: comparing the Isabelle proof assistant, written in PolyML (a multi-core supporting SML implementation developed mostly by one guy) with Coq (which is written in OCaml). Interactive theorem proving in the former is a lot nicer as it takes advantage of multithreading not only for faster concurrent processing of proofs, but also to do things like running Quickcheck and Nitpick in a separate thread automatically to identify trivially falsifiable lemmas, and automatically finding stdlib lemmas that exactly solve a particular proof.
I think PolyML demonstrates that a lack of manpower isn't what stopped OCaml implementing multithreading support. Over the years there have actually been a few proposals/branches implementing some form of support, but all were rejected/abandoned. There was even one that just made the runtime reentrant (passing the runtime around directly instead of having it as a global variable), meaning the OCaml runtime could now be stopped and restarted when embedded in another application (e.g. C calling OCaml), a feature already present in Haskell, but this relatively simple improvement was also rejected (which personally bothers me a lot on a subjective level as I hate globals so it seems like a worthy improvement for its own sake). I remember waiting excitedly four or five years ago for it to be merged, a small but significant step on the path to multicore support, only for that hope to fade away as contributions to the branch slowed to a trickle then dried up completely. Without such extreme focus on avoiding decreases in single-core performance, it would have been much easier for a change like this to have been merged.
I think in recent times there is even less justification for rejecting multicore for affecting single-threaded performance. For two reasons: firstly, the recent addition of FLambda has brought performance improvements in many cases of over 10%, easily enough to compensate for any loss from multi-threading. Secondly, HFT now basically requires FPGA to compete, so single-threaded performance would presumably be of less concern to Jane Street (OCaml's biggest industrial user) now as they really shouldn't be using a software execution engine anyway (disclaimer: I say that as someone working at a competing HFT firm). And if Jane Street isn't doing HFT, then a drop of a few percentage points in single-threaded performance shouldn't affect them much anyway.
Finally, OCaml could always do what Haskell did and add a flag to toggle whether or not multi-threading is enabled, allowing single-threaded users to avoid any performance regression.