[somenewacc]

Type checking your code is, in a sense, a formal proof. That is, your types encode theorems, and the compiler check them.

The article actually alludes to this, linking to this: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[auggierose]

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