Any good programming languages that let you prove correctness (for the most part) and have a function-friendly notation like Haskell, but also let you mutate data in-place for more space- and time-efficient programs?
Are you running into an issue with Haskell in this regard? It’s actually quite possible to write programs which mutate data in-place in Haskell through various monads (the mutation is not visible as a side-effect to the outside world). And because of laziness even some things that are, when strictly evaluated, quite expensive than can be quite cheap in Haskell.
But it seems like the language wasn’t meant for those things. For instance, you don’t see many 3D games or browser engines built using Haskell; C++ is king there, and Rust is aimed squarely at taking over that field. As @Hail_Spacecake said below, Rust might be the closest thing to Haskell that can be used effectively for systems programming.
I’m not really sure what the origin of your question is. Are you making a game or browser engine and you find Haskell insufficient? 3d games and browser engines are fairly large projects, the language isn’t the biggest factor in the decision for those projects. Note, Carmack has been playing with Haskell over the last few years and rewritten some old stuff in it.
For “systems programming”, it depends on what you mean. Many problems people place in the bin of “systems programming” do not have very strict performance requirements. Facebook’s spam detection system has been making waves lately because it has (apparently) a very high RPS and is written in Haskell.
Your question seems to be a classic instance of a premature problem in search of a solution or at least you have not elucidated the source of your question. If you enjoy writing Haskell then write in Haskell until there is a legitimate space- or time-efficiency problem. If you plan on writing 3d games or browser engines then choose languages those industries have settled on.
For some sorta-data, you can read:
I understand that it is possible to write performant code in Haskell; I just find it much harder to suss out what exactly is causing a drop in performance, at least when compared with languages that allow for some state manipulation.
Rust has a Haskell-like type system while still allowing opt-in mutability
I’m curious, not because you are necessarily wrong but just because I’m not sure in what way you’re qualifying this but: what about Rust’s type system makes it Haskell-like? For me, the diverge quite quickly and dramatically.
One possible answer:
Clojure is a dialect of Lisp, and shares with Lisp the code-as-data philosophy and a powerful macro system. Clojure is predominantly a functional programming language, and features a rich set of immutable, persistent data structures. When mutable state is needed, Clojure offers a software transactional memory system and reactive Agent system that ensure clean, correct, multithreaded designs.
From the Haskell wiki:
Haskell computations produce a lot of memory garbage - much more than conventional imperative languages. It’s because data are immutable so the only way to store every next operation’s result is to create new values. In particular, every iteration of a recursive computation creates a new value.