There are tasks which aren’t literally superhuman in that humans can do them, but so few it hardly matters.
Using an SMT solver is soft superhuman. Separation logic is soft superhuman. Theorem proving is soft superhuman. Using Haskell too. Rust is not.
All these tools are just too hard for most programmers/people to learn. But they are very powerful and most of all, an AI can do any of them.
There used to be a debate between automated and interactive theorem proving. In short, automated means using an SMT solver and interactive means using Lean. But both were and are out of reach for most.
Unless you use the AI. But if you’re going to do that, the new economics of the situation say you shouldn’t stop halfway. Use the most powerful tool even if it’s obscure because it scales better.
Lean over an SMT solver. Separation logic over the borrow checker. Instead of an 80/20 solution, go for the 99/1. It’s all the same to the AI. Maybe better not to start, but if you go down such smarty pants paths you should pursue them all the way to the end.