3 ms·
The idea of "programs as propositions" espoused here is in apparent conflict with the more widely known Curry-Howard correspondence [1], which states that progr
by cyrus_ 16y ago
The idea of "programs as propositions" espoused here is in apparent conflict with the more widely known Curry-Howard correspondence [1], which states that programs can be interpretted as proofs and _types_ are propositions.
[1] https://secure.wikimedia.org/wikipedia/en/wiki/Curry-Howard_correspondence https://secure.wikimedia.org/wikipedia/en/wiki/Curry-Howard_...
- sid0 16y agoI'm not familiar with Wittgenstein (it's on my list), but I wonder if the difference is in the system of logic followed (intuitionist vs classical).
- merijnv 16y agoUnlikely, intuionist and classical logic are not fundamentally different. The only difference is that the law of excluded middle (A or (not A)) is an axiom (i.e. assumed to be true) in classical logic.