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.

[0]https://github.com/Z3Prover/z3

[1]https://nim-lang.github.io/Nim/drnim.html