Obviously a language needs to be capable of expressing laziness (which requires closures and some mutability), but it being the default is the issue in Haskell,

Obviously a language needs to be capable of expressing laziness (which requires closures and some mutability), but it being the default is the issue in Haskell, since basically everything returns a closure computing the value rather than the value itself, which is really weird and unexpected, and causes unintuitive (at best) memory usage. As for implicit parallelization with no annotations at all, the main Haskell implementations don't seem to do it, so I guess it just doesn't work (the reasons probably being that there are penalties due to caches being CPU local and the cost of synchronizing threads that make automatic micro-parallelization much worse that explicit coarse-grained parallelization, unless the micro-parallelization is done in hardware by the CPU out-of-order logic). And obviously a type system with controlled mutability like Rust's allows to express explicit parallelization just fine (in fact, writing a safe explicitly parallelized web browser in Servo was one of the main goals of it). > What you really want is a static checker that only prevents shared, simultaneous mutability but admits everything else. The Rust borrow checker is an important step in that direction but it's not it. Is there any example of a static checker that allows more expressive programs than Rust's while preserving the same guarantees? (and without requiring extra annotations like programmer-supplied proofs or using best-effort automatic theorem proving). Is that even possible?