Formally proving something is just very expensive. The difference between the cost of an informal understanding of the correctness of your code, and the cost of formally proving it in a theorem prover is usually at least one order of magnitude (if you are lucky).
A compiler though with a type system actually REDUCES your cost. So these are very different beasts.
Yeah, I should have been more specific in my comment: I don't mean type systems like in Agda or Idris or Coq ..., but where writing down the types is not a big deal, because otherwise you are doing theorem proving with all the associated costs.
In short: I like both my type systems and my theorem proving without any involvement of Curry-Howard :D
A compiler though with a type system actually REDUCES your cost. So these are very different beasts.