Comment by tylerhou

> - Rust's ownership restrictions are harsh. Can we keep the safety and do more?

https://www.languagesforsyste.ms/publication/fearless-concur...

> -- Should compilers have SAT-solver level proof systems built in?

They already do. The exhaustivity checker in Rust (and functional languages) is equivalent in power to SAT.