The Hardest Problem in Type Theory - Computerphile
128,356
Published 2021-07-30
More of Thorsten on Type Theory: bit.ly/C_Thor_playlist
Thorsten's paper dedicated to Martin: bit.ly/C_Thor_Paper
www.facebook.com/computerphile
twitter.com/computer_phile
This video was filmed and edited by Sean Riley.
Computer Science at the University of Nottingham: bit.ly/nottscomputer
Computerphile is a sister project to Brady Haran's Numberphile. More at www.bradyharan.com/
All Comments (21)
-
RIP Martin Hoffmann :( Very sad story. He was my professor, so it hit us students hard.
-
you know the camera guy is lost when he hasn't said a word for 20 min straight!
-
"people at the time when this was a problem said, oh yeah it's easy, we can do it and then went away and said oh hang on it doesn't work" so many problems are underestimated like this.
-
6:37 Iconic: "… because I am a computer scientist, ja." 🤘
-
You made me cry the first two seconds. He was supposed to be my bachelor's thesis advisor, but went missing before we got started. Such a loss for the world. I'll never go hiking alone.
-
Loved this! More Type Theory please!
-
“If I replace both with refl, so I have to prove that relf is equal to refl then i refl”
-
Please, enable automatic subtitles. Non English speakers have a hard time understanding this man accent, and subtitles help a lot.
-
When one knows the depth that this professor knows, it is irrelevant which side goes outside on your tee-shirt.
-
I think I was following along right up until the Professor started talking.
-
Prof T always has amazing explanations. RIP M Hofmann. Will be happy to see more about type theory on here.
-
I've been working on a programming language where equality of types etc are necessary (for example, are two state machines equal even if they are encoded differently), and this video was very beneficial to my research. When you mentioned how a simple boolean can be encoded in different ways, it made me feel like there is information about what I'm looking for already out there and that I'm not in some obscure dead zone that hasn't been entered before. (edit: I probably phrased this comment very badly haha)
-
I studied the intuitionist Martin-Löf type theory in a course this year, it's really interesting but so obscure argument that few know. I would like other videos about this topic So sorry for Martin Hoffmann.
-
When it comes to understanding formal systems and the limitations of proofs you can't do much better than "Gödel, Escher, Bach: An Eternal Golden Braid" by Douglas R. Hofstadter. Everyone interested in math, computers, science, or philosophy should read this classic (or at least as much of it as you can before the binding disintegrates). It will change how you see everything and inculcates a true appreciation for the challenges we face in obtaining that elusive thing we call "truth."
-
interesting way to frame problems, as a programmer I'm used to thinking in the context of math or object related sets, but this looks like an interesting means of standardizing a mixture of the two to kind of more directly reason about it, and specifically a more direct means of incorporating logic through proofs
-
This is the type of presentation that motivates the viewer to want to learn more. Excellent Professor Altenkirch!
-
Computerphile videos with Thorsten Altenkirch from 2017 make me seriously interested in homotopy type theory and type theory in general. So I want more videos about this subject on this channel. PS. I still try to crack syntax of type theory.
-
Great video! I also like how Thorsten used continuous form paper during his explanation.
-
This provides some context to homotopy type theory since fundamental groupoids can be used
-
It clicked for me, thanks for the explanation
