4 ms·
The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable.
by draw_down 8y ago
The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry.
- seanwilson 8y ago> The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry. Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris). I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
- giornogiovanna 8y agoThe simplest place to start, in my opinion, is [0]. If you understand that, then the fact that types are propositions and proofs are values of those types seems pretty obvious. [0]: https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...