Shout out to F#. I think it does a lot of this, doesn't get much respect I think because it is from MS and runs on .NET.
Love the type checking, which I think is better than Rusts. But since I think Rust will win the market, I hope it improves.
I believe, Nim also has this functionality, although, it uses the [0]Z3Prover tool with a nim frontend [1]DrNim for proving.