Programming with Math | The Lambda Calculus
133,003
Published 2024-06-14
After a brief tour of a simple type system, we'll see why the Lambda Calculus has some surprising applications in the field of mathematical logic, and how the implications of this relationship could alter the way that we study mathematics forever.
― Timestamps ―
0:00 - Intro
0:42 - Definition
5:30 - Multiple Inputs
8:10 - Booleans and Conditionals
13:11 - Simple Types
16:32 - Curry-Howard Correspondence
20:58 - Outro
― Credits ―
All animation and voiceover created by Eyesomorphic.
Lean4 proof of infinitude of primes taken from mathlib4 under Apache 2.0 license: github.com/leanprover-community/mathlib/blob/maste…
Background music: 'Reminisce', composed by Caleb Peppiatt.
― Further Reading ―
Types and Programming Languages, by Benjamin C. Pierce (Book)
Category Theory and Why We Care, by Eyesomorphic (Lecture series): • Category Theory and Why We Care
― Corrections ―
At 4:35, the word 'comptuter' should obviously be 'computer', sorry about that!
An entry to #SoMEPi
All Comments (21)
-
The phrase "we know it's correct because it type checks" has blown my mind. I must learn more about Curry-Howard correspondence now
-
This video is super good. Multiple times throughout the video, I was like "ok this does not make any sense" and then immediately after saying that, you said "That seems confusing. Let's look at an example."
-
halfway through the video I suddenly understood Haskell
-
One of the things I took away from reading Gödel, Escher, Bach (mumble, mumble) years ago was that computer languages don't differ in their ability only in their expressiveness . In other words, any language (of at least λ-calculus complexity) can do what any other language can. It's just easier to express in some.
-
as someone who loves both maths and programming, this is probably my favourite math video I've ever seen
-
7:30 "This method...is named currying after the magician Haskell Curry." I'm sure advanced mathematics seems to be magic to some people.
-
so what your saying is i can write every single python program in one line
-
that's nice, now print "hello world"
-
Years of fp propaganda from my friends; And it is this video that finally convinces me it is in fact worth the effort
-
And if you've ever had the privilege of writing Haskell code, it uses the same kind of type checker using an algorithm developed by Milner and Hindley to prove that your program is 100% type-safe, which actually means that if your code compiles, there's a decent chance it's correct. And if it's not, then your toe definitions aren't robust enough.
-
Lambda Calculus seems like the Functional version of a Turing Machine. Very interesting.
-
As a computer science student that studied functional programming and mathematics, I absolutely love this video. Please keep going!
-
This video is amazing! I encourage everyone to watch the video, and then grab a pen and paper and rewatch the video, trying to get ahead of what is being shown. I tried that and realized that I hadn’t actually understood many of the things in the video, like the notation. Videos like these are so well explained that you often feel like you understood everything. But then when you grab pen and paper you realize that there’s many details that you missed. And by the end of it, you feel like you truly understood 90% of it
-
This is why i pay for internet. Thank you very much. I did not pay much attention in class , but if the class was explained like this it would have been awesome.
-
11:00 - "there aren't any y in M" If only Coq would accept this as a proof every time this one detail comes up...
-
I’m a linguist, not particularly mathematically inclined, and honestly, I can’t believe I understood half of it. Incredibly simple yet intuitive. I love the visuals too! Please keep up the good work! :))
-
Wait, this was released 10 days ago? I swear I come back to watch this every 6 months
-
Alice is so obsessed with Java.
-
Great timing! I've always wanted to share this with my friends but I find it extremely hard to explain. It's nice that you made it accessible to others without much experience in math.
-
This reminds me of that MIT video from '86 talking about the eval / apply loop at the core of Lisp. "MIT Structure and Interpretation of Computer Programs" "Scheme / Lisp"