[schrodingerzhu]

The fact is that in many languages, type checking and type inference are coupled together (for languages with DT, bidirectional type checking is needed). When writing proofs, it is almost impossible to let user specify every type.

Ok, let’s go back to normal imperative programming. What about alias analysis? What to do with devirtualization? You NEED type inference. That is being said, I am not a fan of the “usual” ocaml’s style where ppl seem to write as less type annotations as they can. That is not user friendly.