8 ms·
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,
by somenewacc 9y ago
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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- auggierose 9y agoYeah, 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