Curry–Howard correspondence Hah! Found you – knew something like this must exist.

Hah! Found you – knew something like this must exist.
I was going through Mathematics 1001 [from back to front, as I like going from hardest to easiest, as it usually works out that the most interesting stuff is the most complex and the ‘building blocks’ only become interesting once one has tackled the complex… at least for me.
Anyway, I kept tripping over something called “Intuitionism” and a guy named L. E. J. Brouwer, and I _really_ liked what the book said about him.
So, I looked him up. Sad biography but it happens. Explosive period of time in mathematical theory.
So, learned a little about Intuitionism – a mathematical logic theory that was part of the Constructionism way of thinking (which I always found attractive generally – both constructionism and deconstructionism in other fields were always interesting to me) – and tripped over something I’ve been wondering about for a long time:
Why is the logic used in PROGRAMMING look so DIFFERENT from this stuff I see called LOGIC?
I mean, I can do things in programming that are downright forbidden in logic. Why do *I* get that flexibility and they don’t?
Well, I found it. Intuitionism Logic (which I’d never heard of) and programming … or “proofs-as-programs and propositions- ” — well, anyway, it’s still a little over my head yet but I can see this is where smarter heads than mine (so far) figured it out.
I’ve been complaining about the “law of excluded middle” for a long long time because it was never an issue in programming, not really, so I couldn’t understand why it was so darned important in most mathematics and logics. Well I guess not all.
Sorry for the babble but I’m just glad I found this. I hope it leads me in the direction I was looking for but it seems like it is.

Leave a comment

Your email address will not be published. Required fields are marked *

nine − = 4

Leave a Reply