It sounds to me like you might enjoy SML or OCaml.

The ergonomics of both are more oriented towards functional programming rather than imperative. Rust is still primarily imperative with great APIs for functional programming.

Have you had a look at F#?

It has great GC piggybacking on the huge amount of efforts going into dotnet, each release since dotnet core has just gotten faster and faster, not just GC but many parts of the ecosystem, see e.g. https://devblogs.microsoft.com/dotnet/performance-improvemen...

Pattern matching is first class. See e.g. https://docs.microsoft.com/en-us/dotnet/fsharp/language-refe...

I haven’t programmed with traits, but sounds like interfaces which you can have records implement. https://gist.github.com/robertpi/2964793

Function signatures are usually not needed due to the type inference algorithm, so while it is statically typed, you often don’t need to write out the types of functions.

You might enjoy Cone, which is basically Rust with GC (and RC, and any other strategy).

Unfortunately I'm getting certificate errors on their website.

Scala is my go-to for cli tools these days because of that, and even more so since it has a compiler to native (via llvm)

Absolutely, I think there is a huge opportunity here. A rust+gc lang which has seamless ffi with rust would be a killer in my opinion.

Not just seamless, I want it to use rust libraries natively and basically be rust under the hood. Think coffeescript but for rust. The problem with most people's suggestions will be that it deviates too far from rust (giant VMs) and a new language would need a duplicate ecosystem.

I like Rust but I’d use this for so many things!

I feel like this is an inevitability at this point. Kotlin is basically this, and C#/Java/Typescript are getting there, albeit with some historical baggage that might make it slightly less ergonomic.

Lean the theorem proving language?

Indeed, though I have no quote or link for this "claim".

Well, functional programming is very natural for theorem provers, especially those based on the Curry-Howard correspondence.