Your inclusion of FP is interesting in an unintended way: LLMs actually thrive in a highly constrained system like you describe. "It's hard to switch your mindset" - isn't nearly as true for an LLM, it can usually adopt those languages quite readily.

LLMs don't particularly care how hard the type system or borrow checker is (as long as it has good error messages that can guide it to a solution), they can grind away at these things, and what you describe as a negative actually becomes a strong positive. I think we'll see strongly typed systems plus some level of formal verification become popular as an AI-preferred language.

When the burden of review is lowered because you have purely functional building blocks, with lots of formally verified chunks - people will choose that simply out of (productive, beneficial) laziness. Not to mention we're in a ram crunch, and being able to run your stuff far cheaper has an immediate financial incentive.