I'm not sure how much of it has been proven, but this language helps a lot with correctness in software engineering. The compiler and type system conspire to make the software correct when it compiles more often than not. Maintenance work on projects is easy because you never have some global state to worry about, instead, everything you need to understand a function and modify it is in that function's definition.

And nice libraries. But other languages have them bigger and of similar quality.