Rust doesn’t have a very expressive type system. Rust type system would have been at home twenty years ago. Ocaml already had a better type system when I used i

Rust doesn’t have a very expressive type system. Rust type system would have been at home twenty years ago. Ocaml already had a better type system when I used it professionally in the 2010s and they have added a lot since and you could already type infer everything. I’m sorry but implying that having typing becoming a bit more popular is a significant step towards formal proof is akin to saying we are getting closer to using efficient heating because we have switched from burning peat to coal.