Wow, never thought I'd hear HoTT on computerphile! It's hardcore! It's a really new idea and quite abstract, and I don't know any languages or systems which apply them yet. Maybe in the extended interview... 🙂
Thanks. A nice condensation of Voevodsky's ideas/program in this short video. I keep wondering how the theory of Types can handle the implications of the work of Kurt Godel, or a questions like the Continuum Hypothesis which as we know is independent of Zermelo Frankel Set Theory. I hope Vladimir's program does not die with him. His death is a great loss.
What gets to me is even after 3 years he is still the top 10 highest contributor to this theory of math on github. What happened to that 50k people watching this video? Don't they get that literally anybody can be a mathematician, given a computer?
It's hard to boil down someone's life work, especially when you're trying to explain transitivity between analogous types - using analogies isn't exactly fair. :) If I understood correctly, he encoded mathematical properties into traits, and any proof in a strongly typed context that references properties from a set of traits applies to any type that derives from those traits. Application to a type that doesn't derive from them is a substitution failure (compiler error) so successful compilation and proof of what you've encoded are one and the same.
I'm sad that I learned of his passing for the first time through this video. Homotopy Type Theory is such an amazing project, I hope to be able to contribute to its growth during and after my graduate studies. Rest in peace, Prof. Voevodsky. T_T
Voevodsky is Polish Wojewódzki. Generic Polish surnames ends on -ski, Russian ends on -ov. So it should be Ivanovich Ivanov. Well, actually Ivan Ivanovich Ivanov.
I don't think that was the point of the video. They did a whole separate video, plus Extra Bits, on Type Theory. This was about Vladimir Voevodsky's death, not Type Theory.
I never have any sound when watching computerphile over my speakers. It works fine on my headset though. I don't know what's up with the sound settings on this channel.
the videos are mono - its possibly a single channel thing, or that the speakers are out of phase and cancelling each other out, or perhaps due to the bitrate? Sorry to hear this >Sean
the video mentions how homotopy type theory tries to group equivalent types, eg natural numbers represented in binary and natural numbers represented using 0 and successor. But if we were to create a type that represents a Turing Machine, it has been proven undecidable to determine if two Turing Machines are "equivalent" (accept the same language), so doesn't that make homotopy type theory impossible?
It is only impossible to have a general algorithm for deciding if two Turing machines are equal. Given the type of Turing machines, two of its terms could be proven equal "manually".
I would like to insist that equality is undecidable especially under the univalence axiom, precisely because both things are "as worth as" (equi-valent) each other, so one cannot tell them apart functionally (still structural or ontological differences may hold).
Tools can be perfected over time and you can add tests to make sure the tool stays at a certain standard level of correctness. The human mind has no such checks nor sustainable improvements over time. You tell me which you'd rather trust? :)
Just as you would use 3 compasses when you absolutely want to be sure where north is, you get multiple samples from different tools when you care about proofs.
We actually have a proof that the Coq proof assistant Prof. Altenkirch was talking about has no bugs. In fact Voevodsky wanted to make sure the logic was airtight so bad that he only used the fragment of Coq's type theory that he knew was consistent with homotopy type theory, and never any of the experimental features.
the human. but you admit that human brain is defective, and so it must not be trusted, yet, in the same breath you trust tools created by said defective and i assume defunct human brain. divide by zero much?
The number of likes on this video is mind boggling. Without constructive criticism and honest feedback this channel will never improve. Why do you guys think Linus Tech Tips has like 5 times more subscribers than Computerphile? Because people are not afraid to be honest and *DISLIKE* when mediocre content is uploaded! Then they improved and look at them now!
This video is not about the content, it's about remembering a great mathematician, who has died recently. If you feel like this type of video is not close to your standards, just dislike and move on. There's no need to rant about it.
Come on, Linus Tech Tips is just clickbait that delivers, and that's why it's popular. Also computer science is not as popular as "consumer geek culture".
Sad to see him go but at least he contributed greatly to mathematics before passing. Many of us can only dream of such an accomplishment.
Callum Hays many?
Wow, never thought I'd hear HoTT on computerphile! It's hardcore! It's a really new idea and quite abstract, and I don't know any languages or systems which apply them yet. Maybe in the extended interview... 🙂
He mentioned one, Coq.
This guy looks like that eccentric professor from a cyberpunk thriller the main character has to track down.
🤣
RIP one of my heroes in math.
Still no closer to understanding homotopy theory.
Try the 'extra bits' ? >Sean
Still no closer to understanding what this guy's saying
Button don't work
I don't speak English but still listening
Thanks. A nice condensation of Voevodsky's ideas/program in this short video. I keep wondering how the theory of Types can handle the implications of the work of Kurt Godel, or a questions like the Continuum Hypothesis which as we know is independent of Zermelo Frankel Set Theory. I hope Vladimir's program does not die with him. His death is a great loss.
What gets to me is even after 3 years he is still the top 10 highest contributor to this theory of math on github. What happened to that 50k people watching this video? Don't they get that literally anybody can be a mathematician, given a computer?
uhhhhhhh that's probably a bit too far...
Ah yes because everyone knows there's no sort of barriers to mathematical knowledge 😜
@@jmw1500 way to go, you missed the point
Cool stuff. Would like to know more about the proof assistance tool he mentioned Koch?
coq.inria.fr/
Thanks very much for the prompt response.
Did he mean polymorphism in a way that the compiler predicts from the calls how the structure must look like?
I'm beginning to think the Fields Medal is cursed! Earlier this year it was Maryam Mirzakhani, 40, who was one of the last winners.
these are very great lost for humanity :(
@Computerphile Would it be possible for you to interview some Computer Systems Architecture theorists and engineers?
How do you get to the extra bits?
+velcrorex th-cam.com/video/Ft8R3-kPDdk/w-d-xo.html
This is like if that guy from flight of the concords was a mathematician.
Damn, a sophon got to him... RIP
The video links at the end to extra bits don't seem to work just FYI.
So he basically said the same thing 3 times even using same words?
It's hard to boil down someone's life work, especially when you're trying to explain transitivity between analogous types - using analogies isn't exactly fair. :) If I understood correctly, he encoded mathematical properties into traits, and any proof in a strongly typed context that references properties from a set of traits applies to any type that derives from those traits. Application to a type that doesn't derive from them is a substitution failure (compiler error) so successful compilation and proof of what you've encoded are one and the same.
I used to think that this channel didn't get far enough into the nitty gritty, but over the last few months, that's not been the case at all
I can't wait for the followup
I admired your videos till the point where i see a mic cable outside and it didn't even a bit matter
There is a link between Voevodsky and myself, a coincidental mathematical link. He was born 1 year, 1 month and 1 day after me.
Can someone post a link to the extra bits? The in-video link isn't working for me (and I thought it was phased out in general.)
I'm sad that I learned of his passing for the first time through this video. Homotopy Type Theory is such an amazing project, I hope to be able to contribute to its growth during and after my graduate studies. Rest in peace, Prof. Voevodsky.
T_T
I'm really sorry but all I can hear is a 'rooster' system - what is the proof system?
Rpz les abonnés de Science4all !
Ouaaais
One of the most russian name after "Ivanovich Ivanovski"
Tengku Izdihar You mean Ivan Ivanovich
Because he is Russian? Strange, huh?
Ivanovski sounds like a polish surname.
Voevodsky is Polish Wojewódzki. Generic Polish surnames ends on -ski, Russian ends on -ov. So it should be Ivanovich Ivanov. Well, actually Ivan Ivanovich Ivanov.
coq system
The point of the video isn't until 4:27...and its a 6 minute video. I love you computerphile but this video wasn't up to computerphile standards.
I don't think that was the point of the video. They did a whole separate video, plus Extra Bits, on Type Theory. This was about Vladimir Voevodsky's death, not Type Theory.
The title: "Homotopy Type Theory: Vladimir Voevodsky - Computerphile
"
I'm pretty sure it IS about type theory.
Clean that mouse!
How do i turn on sound?
*Explaining what the fields medal is*
I think everyone watching this video already knows what it is lol
oh hey look
This is interesting, but someone sort out that whiteboard. This is the second time I have seen that monstrosity behind Thorsten. *triggered* ;)
I never have any sound when watching computerphile over my speakers. It works fine on my headset though. I don't know what's up with the sound settings on this channel.
Faxter313 what the h*cc
the videos are mono - its possibly a single channel thing, or that the speakers are out of phase and cancelling each other out, or perhaps due to the bitrate? Sorry to hear this >Sean
the video mentions how homotopy type theory tries to group equivalent types, eg natural numbers represented in binary and natural numbers represented using 0 and successor. But if we were to create a type that represents a Turing Machine, it has been proven undecidable to determine if two Turing Machines are "equivalent" (accept the same language), so doesn't that make homotopy type theory impossible?
It is only impossible to have a general algorithm for deciding if two Turing machines are equal. Given the type of Turing machines, two of its terms could be proven equal "manually".
Who says that equality has to be decidable?
I would like to insist that equality is undecidable especially under the univalence axiom, precisely because both things are "as worth as" (equi-valent) each other, so one cannot tell them apart functionally (still structural or ontological differences may hold).
He really hasn’t said anything in this video that teaches a neophyte something new. I don’t think this video was worth posting.
clean your damn desk bro
risingpower lol. If you think his desk it's a bit little disorderly, you wouldn't want to see my desk.
because tools never have mistakes.
Tools can be perfected over time and you can add tests to make sure the tool stays at a certain standard level of correctness. The human mind has no such checks nor sustainable improvements over time. You tell me which you'd rather trust? :)
Just as you would use 3 compasses when you absolutely want to be sure where north is, you get multiple samples from different tools when you care about proofs.
We actually have a proof that the Coq proof assistant Prof. Altenkirch was talking about has no bugs. In fact Voevodsky wanted to make sure the logic was airtight so bad that he only used the fragment of Coq's type theory that he knew was consistent with homotopy type theory, and never any of the experimental features.
the human.
but you admit that human brain is defective, and so it must not be trusted, yet, in the same breath you trust tools created by said defective and i assume defunct human brain.
divide by zero much?
The number of likes on this video is mind boggling. Without constructive criticism and honest feedback this channel will never improve. Why do you guys think Linus Tech Tips has like 5 times more subscribers than Computerphile? Because people are not afraid to be honest and *DISLIKE* when mediocre content is uploaded! Then they improved and look at them now!
This video is not about the content, it's about remembering a great mathematician, who has died recently.
If you feel like this type of video is not close to your standards, just dislike and move on. There's no need to rant about it.
Come on, Linus Tech Tips is just clickbait that delivers, and that's why it's popular. Also computer science is not as popular as "consumer geek culture".
Evidently, more people want 50% content + 50% infomercial. Your point?
first not to be not to be first
first not to be not first
first