3 ms·

That’s how I understand it now after a bunch of exposure to type theory and internalising Curry–Howard. But as a programmer my earliest practical way of thinkin

That’s how I understand it now after a bunch of exposure to type theory and internalising Curry–Howard. But as a programmer my earliest practical way of thinking of it was “How would I use an ‘implies’ operator in programming?” Things like these: (a => b) == (a ? b : true) == !a || b if (a) assert(b); // == assert(a => b); #if !defined(_MSC_VER) || defined(_NATIVE_WCHAR_T_DEFINED) // == #if defined(_MSC_VER) => defined(_NATIVE_WCHAR_T_DEFINED) if (!p || !p->buffer) return 0; // == if (p => !p->buffer) return 0; That is, just talking about truth values, the results of proofs rather than the proofs themselves.

adrianratnapala 9y ago
This is interesting because, I'm trying to get to grips with where the abstract and the practical meet. But I'm not sure all of your example fit. Your first example if(a) assert(b); really does fit the intuitive idea of implication. The other two just look like cases that happen to have the same boolean structure as implication, but that's not their meaning. For example if(!p || !p->buffer) return 0; Means (roughly) "check if p's buffer exists, which of course requires that p also exists". So there is a kind of implication here, but it goes in the direction p->buffer => p Which is not what you are talking about.
- evincarofautumn 9y ago
  The “#if” example seems clear enough to me. We always want to use wchar_t, but if we’re using MSVC, then only if it’s available. The “buffer” example isn’t great, I agree. I just pulled these from random sources in my projects directory by grepping for “not…or”.
  - adrianratnapala 9y ago
    Your "#if" logic sounds perfectly reasonable, but what does it have to do with implication? Except that the boolean test just happens to have the same truth table.

adrianratnapala 9y ago

This is interesting because, I'm trying to get to grips with where the abstract and the practical meet. But I'm not sure all of your example fit. Your first example if(a) assert(b); really does fit the intuitive idea of implication. The other two just look like cases that happen to have the same boolean structure as implication, but that's not their meaning. For example if(!p || !p->buffer) return 0; Means (roughly) "check if p's buffer exists, which of course requires that p also exists". So there is a kind of implication here, but it goes in the direction p->buffer => p Which is not what you are talking about.

evincarofautumn 9y ago
The “#if” example seems clear enough to me. We always want to use wchar_t, but if we’re using MSVC, then only if it’s available. The “buffer” example isn’t great, I agree. I just pulled these from random sources in my projects directory by grepping for “not…or”.
- adrianratnapala 9y ago
  Your "#if" logic sounds perfectly reasonable, but what does it have to do with implication? Except that the boolean test just happens to have the same truth table.