Marcus G. Daniels wrote at 04/19/2013 09:32 AM: > I'm contrasting compile-time assertions against run-time assertions, and > claiming the former is better when it can be achieved. > http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
That's awesome! Thanks for that link. It proves that I've been lazy. I'll paraphrase this and submit it for ridicule? Until Griffin, the Curry-Howard correspondence was thought to only apply to intuitionist logic. I.e. no proof by contradiction and other magic that relies on the excluded middle. As such, type theory was distinct from program (theory?) because it captures conditions/state that formulae don't. By showing that the excluded middle can be formulated as a continuation, i.e. capturing a particular type of program state, the correspondence holds out to classical logic as well. If that's even close to a decent paraphrase, then it bolsters my sense that types are somehow a state-oriented conception. -- =><= glen e. p. ropella Fire it up, fire it up, fire it up yeah that's the ticket now kick out the jams. ============================================================ FRIAM Applied Complexity Group listserv Meets Fridays 9a-11:30 at cafe at St. John's College to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
