Hacker News Reader

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.

View on HN

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...

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

Reply on news.ycombinator.com