The Curry-Howard Correspondence

What's the most beautiful result you know? For me, it's the Curry-Howard correspondence, which goes by many other names (including "propositions as types" and the "BHK interpretation"). This correspondence relates propositions to types, proofs to programs, and proof simplification to program evaluation.
Recorded live at Bailey Hall, Cornell University, Ithaca, NY, 2019.
Textbook: cs3110.github....

[@nopaniers]

This was beautifully explained. Thank you. I know this is an abstract idea, but it also seems practical - even though they are equivalent, for some reason it seems much easier to come up with programs that produce a given type than logical proofs...

[@vincentm99]

This video was fantastic, thank you very much for this incredible lecture
I learned a ton

[@usercommon1]

Epic

[@seerowyLudek]

Question:
What about mutable variables?
How does constructive logic explains them?
I guess it's somehow related to negation and double negation, but it's just a wild guess (because as I've found ¬A = A->⊥ which we can read as A->void).

[@MichaelRyanClarkson]

For mutability you want to go beyond constructive logic to linear logic. See this paper: Philip Wadler (1990). Linear Types can Change the World! More recent work here: ctp.di.fct.unl.pt/~lcaires/papers/PaT_SS.pdf

[@vincentm99]

Hi! at 7:40 there is are missing helper parentheses on the first proposition:
it should be (a -> b) -> (a -> b)
-> being the symbol for implication
the implication in propositional logic is right associative meaning that:
a -> b -> c a -> (b -> c)
being the symbol for equivalence
that is the rule that was followed when adding the helper parentheses if it was confusing for some
also, a -> (b -> c) (a and b) -> c
that is probably more understandable when you know that ;) (this rule is actually currying)

[@oneofvalts]

Thank you very much. This is a treasury. May I ask the name of the font used in the slides?

[@MDNQ-ud1ty]

It is not surprising that logic and programing are the same. After all, computers are built off logic gates which are just implementations of logic functions. All programming is is a higher level of abstraction to reduce complexity and increase efficiency. It's literally logic under the hood and has always been that way. It would be more surprising if it wasn't that way. It's surprising that humans have been able to build such complicated structures that work so effectively given how screwed up their social structures are.

[@leswine1582]

hm, well, yea, probably

[@alaindevos4027]

Great courses. Al respect. But something i missed. It's afraid of libraries. I mean the practical stuff.
In real world application there is a gui-toolkit in the worst, or a database in the best.
These should be tackeled.

[@jpdiegidio]

That is all very good (thank you), but computation is not reasoning, courtesy GIT... (Mathematical logic is not Logic.)

[@jeffreyjdesir]

Do you think it’s possible to fully correspond logic to physics and causality as well as mathematics?

[@jpdiegidio]

@@jeffreyjdesir Of course I don't, to begin with because Logic (with a capital "L") is not formal logic, etc. Those are all distinct disciplines, meaning their problems as well as their methods. And my point was the Curry-Howard-Lambek correspondence is *totally internal* to *mathematics* (formal logic computation categories). That we are more and more *using* mathematics all over the place doesn't mean Logic or Physics or Economics or Engineering, etc. etc. become a branch of mathematics, and rather the problem nowadays is, in its extreme form, the so called "lying with numbers", which is the form of a fallacious inversion of dependencies and priorities. In short... Hope that helps.