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...
The article actually alludes to this, linking to this: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
In short: I like both my type systems and my theorem proving without any involvement of Curry-Howard :D