Computer Science ∩ Mathematics (Type Theory) - Computerphile

As computers are used more and more to confirm proofs, is it time to take computer science's contribution to mathematics further? Dr Thorsten Altenkirch discusses Type Theory vs Set Theory.
A Longer version of this interview can be found here: • CS ∩ Mathematics : LO...
EXTRA BITS: • EXTRA BITS: Computer S...
/ computerphile
/ 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

[@yepperdeedooda]

I'm starting realize that just because I come here, it doesn't mean I'm smart.

[@kevinpacheco8169]

Ксения Ковалевская lolz...

[@CarlosN2]

You're wandering into the trolls' dungeon, you might find yourself getting too much attention from those who are smart.

[@IllumTheMessage]

It's just learning the terminology. You are smart.

[@yepperdeedooda]

Zod 'kneel before Zod.' You were awesome.

[@yepperdeedooda]

***** I wish it applied to me in class. I'm horrible at math.

[@tzimmermann]

The guy Gérard Huet behind Coq also wrote some data structure he called The Zipper. Apparently he said in conference during a demonstration: "Now I'm gonna open the Zipper and show you my Coq". Source: someone at INRIA who knew Huet told me.

[@kevinpacheco8169]

Terrence Zimmermann Now that you can't make up.

[@tzimmermann]

Kevin Pacheco I didn't. I assume the guy wasn't trying to troll us when he told the story during a dinner (with mainly scientists and engineers), because well, he wasn't the trolling type. And you can check that Huet actually invented the Zipper (a kind of tree data structure). Of course, what I said doesn't constitute a proof, but that's all I have.

[@Foagik]

A Huet Zipper isn't necessarily a tree-like structure, but you can make a Huet Zipper of a tree. A zipper is more or less a structure that gives the notion of a cursor on an underlying structure such that there's O(1) operations on whatever's underneath the cursor, and it has several operations for moving that cursor around said structure. If you want to see some trolling, try out McBridge's presentation to the Haskell Implementors Meeting, '09 about the Haskell Preprocessor.

[@tzimmermann]

+Foagik Thanks a lot for the info, I am undoubtedly uninformed about that kind of structure as I never needed to use one. That seems quite powerful, I've downloaded Huet's paper for further understanding. Conor McBride, right? I don't seem able to find this presentation, is it on yt?

[@PietchRhum]

I've worked with people at the INRIA and that's totally the kind of humour they have! I have no problem believing this story!

[@Ikkarson]

Mathematicians should wear robes and pointy hats and be interviewed in front of some copper plated bubbling apparatuses (apparati?). Then replace "theorem" by "curse", objects by "demons", and demonstrations by "invocation". "First evoke a local Riemann-integrable demon. the Fundamental Curse of Analysis allows you make sure you can restore that demon when you observe its growth." Cedric Vilani is the headmaster of the Lyon School of Wizardry and professor of Implicit Demons Taming.

[@mduckernz]

Antonin Caors haha, yeah 😌 Master of Demon Invocations

[@mduckernz]

Amandeep Kumar Come now, there's not even any DnD references yet! 😅

[@garetclaborn]

what? they are. wait where do you guys live?

[@jeongheonlee4556]

New name for mathematics: demons taming

[@EpicFishStudio]

this sounds just so cool.

[@unvergebeneid]

Drink a shot every time he says "ja".

[@Backbeardjack99]

HGich.T - Tutenchamun, he is clearly a fan ;D

[@sergejnekrasov7688]

Thank you for the advice I'm still laughing!

[@supernewuser]

ja-ger

[@fdutrey]

I cannot unread your comment....

[@CarlosN2]

"Das ich soll!"

[@peanut1110]

Didn't know Thor was into maths

[@ToastiLP]

Hehehehe...get it? Because his name is Thorsten

[@Kram1032]

lol red

[@AndersJackson]

Thors stone...

[@nm18996]

math*

[@arturmizuno893]

it's maths, not math, stop omitting words

[@gulllars4620]

As a programmer, this makes so much sense. I was in a weird situation where i learned algebra first, and then learned programming (and algorithms and data structures), and then more maths, and i couldn't help but think how i could represent the concepts i learned in computer code, but the notation used in maths was set theory, which was slightly confusing some times. Then i noted to a lecturer that a definition he wrote of something could be expressed as a short recursive function, and turns out he knew (among other things) haskell and he agreed that the recursive notation was correct, but pointed out that you can solve some such functions which may be noted recursively using transformations that allow you to do it as one computation instead of a series of computations (iterative), which can dramatically impact the time they take to run, and he had done work on that. Using maths to speed up some heavy logic functions by transforming them. Anyways, my big take-away is i'm fairly decent at maths, but i'm a bad calculator, and i strongly prefer computer science notation over set theory notation. If i had been taught maths through programming the concepts, i would have done MUCH better, and it would also have allowed running the functions and (automatically through code) visualizing the output to gain a better "feel" for it.

[@SuperDrdoof]

As a unsuccessful student of mathematics who went to computer science I think, it's because computer scientists care much more about the style of notation and are better trying to find the right language which describes their current problems.

[@allenx6309]

Wow, this is soo true.

[@dabrownone]

But you can also tail call optimize at the compiler level.

[@lawrencedoliveiro9104]

John McCarthy, the father of LI

[@lawrencedoliveiro9104]

SP, relates how he tried to suggest to mathematicians that functional LI

[@eightrice]

"A function which doesn't function shouldn't be called a function" Real-life James Bond Villain - 2017

[@aperson4051]

I will die a happy man when the producers of James Bond finally hire this man to be their evil genius.

[@VoltzLiveYT]

The jist of the curry-howard correspondence is: In a well-typed programming language (such as Coq, Agda, Idris etc.) Types correspond to theorems Programs correspond to proofs. You write the type, then you prove it by writing a body to that function.

[@ShubhamBhushanCC]

Mathematical Poofs! I love this guy

[@GilesBathgate]

He uses the coq system for his poofs!

[@polishal9061]

Shubham Bhushan is this about Alan Touring :D ?

[@nazgullinux6601]

*Alan Giedrojc* "...Alan Turing"

[@rajshrisukhdeve9200]

@@GilesBathgate bun

[@captain_cloudd]

War is Peace - Freedom is Slavery - Ignorance is Strength.

[@ElagabalusRex]

I think this would have been more clear if we had examples of some useful types that propositions and their proofs could take.

[@Bratjuuc]

I could provide some really simple examples in Idris or Agda, if you're still interested, but it takes a bit of knowledge Haskell-like syntax.

[@gileee]

This was more like a history lesson than an explanatory video

[@bimbumbamdolievori]

Still this is very interesting stuff

[@ivanpiri8982]

@@Bratjuuc are u still willing to provide examples in agda? I'm currently studying this subject and the lack of examples is killing me

[@Bratjuuc]

@@ivanpiri8982 Oof, that was pretty long ago. I forgot what I wanted to provide as examples back then. I'm going to need some time revising, but I'm still willing to provide examples. I would prefer to provide them in Idris purely for syntax reasons. So far I can illustrate the following: *) Boolean logic. *) maybe Existential quantifications I'll probably update the list in a short amount of time.

[@eliastandel]

So it seems our galactic president Beeblebrox is into type theory. BTW, great video! Love this more theoretical approach to Computerphile!

[@JonathanWinterflood]

He must have painted his seond head Pink, too

[@RiRiDingetjes]

Yeah totally agree! Altough I wish he would have written down something

[@filipkralj2618]

"coq could upset english speakers" LOL and they say Germans dont have a sense of humor

[@steliostoulis1875]

cofi 41 French*

[@badradish2116]

i think he meant the speaker, but isnt he like dutch or something?

[@roy04]

@@steliostoulis1875 I think that was intentional

[@MaceOjala]

That was really fascinating. I have heard of type theory but didn't know much more that it resembles types in programming. He contrasts it to set theory which helps a lot and makes sense. What we seem to have here, as he is saying, a potential, qualitative (of course partial) transformation of a field, mathematics, because new tools, computers, bring new paradigms. Fascinating, thank you so much. I would be happy to see some more of this, and maybe some examples from this style of math.

[@illustriouschin]

I'm pretty sure the only people who understood what he was saying already understood everything beforehand.

[@MonkeyboyGoku]

Gordon Chin roughly

[@grn1]

I had to rewatch it but I think I got it down. Abstract math isn't exactly my forte though.

[@dailydoseofcyr2823]

I think if you have a first year discrete math class or even maybe a high school computer engineering class under your belt, you should be able to follow along

[@astroid-ws4py]

First year Discrete Math couse is enough

[@user-tx4wj7qk4t]

Having a degree in CS should be enough to understand what he's saying

[@2Cerealbox]

I think the guy behind this saw us complain about the 404 video and is now giving us some meatier content. I'm happy. :)

[@WWxeroWW.WERWKWWF__WPWWW.-_WWW]

Ja

[@garetclaborn]

ja

[@kimchikoalaa714]

I recently signed up for CS in school, and math class is doing set notation. A youtube title has never been so relatable.

[@uberobserver]

More vids on Haskell and functional programming would be great!

[@MaxPicAxe]

KZbin is great at suggesting videos. I am starting college and covering set theory, and I realized that there are multiple encodings for natural numbers and that implementation details were being exposed. And then I find this video which mentions the same thing. Amazing.

[@Aaku13]

Man, this dude is so intelligent. He just pulls all this theory history out of his head; its awesome.

[@jamma246]

Thorsten is a great explainer and talks about some really subjects - liked this video! You guys should also track down Kevin Buzzard. He's a great speaker, interesting guy, and he's recently been working on proof formalisation in a language called Lean. He and students have been writing up a whole bunch of definitions/theorems/proofs, and is planning to do his whole department's curriculum.

[@OwenPrescott]

Need a proof? Bring on the COQ.

[@wfwfrsf2168]

cringe

[@lorenzvo5284]

Proof theorems ja. samsing wrong wis se pruuf.

[@rusduderus]

Ja?

[@uberobserver]

Excellent video on a relatively new field of study with a real future!

[@avibank]

This is exciting. Just finished Group Theory and this seems like something I can learn from a text book now.

[@FreeScience]

I was surprised that he managed to talked about set, type and homotopy theory, abstract mathematics and new foundations of mathematics without mentioning category theory.

[@mdmenzel]

Calle Silver-Granhall I think because category theory is more difficult to explain to a general audience than the other three. Also, previous videos have alluded to type theory and set theory.

[@mikidep_old]

There is some on the whiteboard on its back...

[@AnarchoAmericium]

I doubt it. Category Theory isn't hard.

[@abenezerfetsum3632]

Literally every thing he mentioned would have been way easier if he did a quick recap of category theory and what it is. I mean basically everything he talked about was under category theory.

[@kithsakhai]

great video hope to see more abstract discussions like this for more computerphile videos! or at least a numberphile video on this but more from the other guys' perspective.

[@DeoMachina]

I like listening to Dr Thor here But I'm gonna be honest, I got lost about 5 minutes in :(

[@platosrepublic6965]

DeoMachina I was lost in his "ja"s.

[@AlexaDeWit]

His name is Dr. Altenkirch. He's not nordic either.

[@heimdall1973]

Mark, that's because the implementation and representation don't matter. As Dr Thor said, you have 1+1+... or binary or decimal... It also doesn't matter what shape the symbols are. I was surprised to find out that the Predators use decimal system the same way as we do, just that symbols for 0, 1, ..., 9 are those funny patterns.

[@rcookie5128]

haha "Dr Thor", really like it, esecially when i read its an abbeviation of his real name..

[@Nim2]

I know I'm late but props to the one(s) who made the subtitles. Very creative with using the relevant symbols.

[@phpngpl]

Underneath Type Theory there is a more foundational mathematical approach called Category Theory, which seems to unify all areas of mathematics. Unsuprisingly, Types form a Category. Just as there is a connection between Homotopy Theory and Type Theory, there is a connection between eg. Set Theory and Topology Theory via Category Theory and the theorems of one theory correspond to theorems of the other. I suggest you look into that.

[@worldboy9684]

This is awesome, my mind is blown and I feel much better

[@jimamsden]

I think of mathematical proofs as a mechanism for problem-solving and gaining understanding while producing useful outcomes. Consider machine learning vs. algorithms. Machine learning can develop a function based on a training set that we can use to predict results from other inputs. That's great, but it doesn't necessarily lead to expanding our understanding of the underlying principles, things that we can use to help solve other more general problems.

[@OwenPrescott]

This guy takes no.3 spot after the Klien bottle and Japanese guy.

[@patrickwienhoft7987]

No way. Matt and James come before him by a long shot.

[@Ludix147]

Patrick Wienhöft but they are over on numberphile ;)

[@OwenPrescott]

Patrick Wienhöft I'm talking on the "looks like science/math" scale. Although I think James could compete with this guy. Oh I forgot the Chemistry guy too!

[@AlRoderick]

I was going to say, no one looks more like science than Prof. Sir Martyn Poliakoff.

[@patrickwienhoft7987]

Well, then Tadashi shouldn't be there. He just looks like an ordinary Japanses. The chemistry guy obviously belongs in there then, yes ^^

[@isaacdavid2491]

gotta love the category theory diagrams on the back

[@Ludix147]

this is really awesome and interesting, I will check out set and type theories!

[@jayjeckel]

We are happy to welcome you mathematicians into the programming world, but there is one thing you need to learn fast and constantly repeat to yourselves if necessary: Single character identifiers are not acceptable! Use full words and clear and consistent naming conventions. Learn it, live it, love it.

[@joses.5943]

could we have a second video perhaps going more into detail of type theory maybe xsome examples of its uses. pls

[@honkatatonka]

Ok, the comments have spoken: "Dr. Thor" it is Edit: very interesting! Thanks for doing these!

[@rogierbrussee3460]

Surprising as this may seem, Mathematicians seldom bother with sets in practice. In fact they already use mathematical constructions pretty much exactly like how it is described with types. For example the natural numbers N, defined as a set together with a preferred element 0 and a function s:N ->N that gives the successor (programmers would call it next) which is "universal" with this property (in the precise technical sense below), is enough to define N unique up to _unique_ isomorphism (= bijection), and that is perfectly good enough to work with it and ignore any implementation details and it nicely avoids asking silly questions like whether 2 \in 3 because they are not preserved under these isomorphisms. Here a set of natural numbers (N, 0 , s) is _universal_ if it has the following property: for any set X, element x \in X and any function T:X->X, there is a unique function f: N->X such that f(0) = x and f(s(n)) = Tf(n) (from which it easily flows: f(n) = T^n(x)). Of course one now has to prove that such a set exists (surprise surprise, it does).

[@user-tx4wj7qk4t]

This is still an implementation detail. Type theory and category theory abstract away all of this and just have the type N. What you're describing is a declarative but iterative way of describing a set, which really isn't any better from my perspective than set builder notation, which is also declarative and how the highest abstraction of iteration is expressed in functional languages. In fact what you're describing is two levels of abstraction lower than set builder notation which is considered implicit iteration while the iterator you're describing here is external iteration

[@thesam723]

I super enjoyed this video

[@mazed363]

I've always struggled with gaining intuition in abstract mathematical theories because of the set theoretic foundations, (set theoretic definition of topology, for instance)

[@DavidVaughan00]

Eyyy funny stuff, I just used Coq a month ago for researching a class project. I was writing a paper on using recurrent neural nets to automatically write proofs in a Coq-like language. I was not successful - turns out it's pretty hard to do, lol

[@GordonjSmith1]

Really informative and 'enlightening'. My thanks.

[@EDYMOT4991]

can you make videos explaining type theory and how math ideas can be proven with it?

[@orlinzer123]

Please do video on backpropagation algorithm in neural networks

[@JohnnyDoeDoeDoe]

or linzer computerphile, don't be afraid to get a bit technical!

[@mrnarason]

or linzer 3blue1brown did that video recently

[@StarLink149]

For those who don't know, "coq" means "rooster" in french.

[@hankigoe829]

Top 10 programming languages to learn in 2020: 1. Type theory 2. Type theory 3. (wait for it) Type theory ...

[@garetclaborn]

So this may be way off, but is SFINAE (in C++ templates) for type deduction basically using the same relationship to encode logical statements?

[@stevecummins324]

Set theory has the concept of universal set on which a choice function to extract a particular set can be applied.... Like moving from from everything towards being specific. Does universal set include everything that might be constructed?

[@GeorgeLabuschagne]

Could this be used to assist with the verification of the proof to the ABC conjecture?

[@matrixstuff3512]

I like to think that I know quite a lot about both mathematics and computer science, but this goes way over my head

[@animowany111]

Could you talk about the Haskell type system?

[@Bratjuuc]

Not as rich as COQ, Agda or Idris ones

[@1000animeboy]

This guy looks like the scientist from Independence Day!!!

[@BarnezGFX]

he's my lecturer! top top guy

[@ChrisHinton42]

It will be interesting to see if a type theory is developed in which univalence is a theorem rather than an axiom

[@ThorstenAltenkirch]

Check out the cubical system made at Chalmers university.

[@macchiato_1881]

I have been studying formal mathematics for my Computer Science thesis for a little while now. And looking back on it, I think Set Theory has its priority backwards. Set Theory tries to take two Sets of elements, and tries to evaluate whether a function definition exists as a pathway between these two sets. Type Theory takes a set and a function definition, and uses it to generate elements of another set, which can be used as proofs for the other set. How I understand it is that: Set Theory is like a funky subset of Type Theory because Set Theory deals with concrete definitions generated from abstract ideas, whereas Type Theory works the other way around. In a way, this is more useful and powerful than Set Theory because you can easily create various definitions of a set of elements that would otherwise be hard to do using Set Theory. It's not impossible. It's just hard...

[@TheodoreWard]

If it is unable to distinguish between different representations of numbers, is it impossible to do boolean algebra? Is it possible to calculate the result of 42 AND 69 for instance without representing the numbers in binary?

[@jandobbelsteen8953]

I just watched this video and to my understanding using HOTT you would be able to show that in fact two different proofs have the same outcome and thus are the same. So you would be able to first create a proof and then verify that in fact it is an improvement (more elegant, easier, whatever) to an already existing older proof... ? Or, the other way around, you would be able to show that a proof is really different from another proof...?

[@amberstiefel9748]

10:49 he is onto something imo Aesthetics and genres and psychology and visual mediums paired with endless user data

[@jakejakeboom]

such a great thumbnail

[@shintsu01]

COQ magic :D

[@dukeradwardthe5th843]

Can't be misinterpreted at all, eh?

[@FreeScience]

The Gathering?

[@josnardstorm]

Wow. Brady's really bringing in the big bucks. He brought in the scientist from Independence Day.

[@davidgillies620]

Formal methods are getting more and more important as systems grow. For things like blockchain processing one approach to proving correctness is Hoare's Communicating Sequential Processes. Then there's Predicate Transformer Semantics etc.. It all gets very complicated.

[@sammclennan3661]

More videos of this guy please. I have no idea what he's talking about but... more videos please.

[@Zero0exe]

6:43 or as Mr. Numberphile would call it: The Parker Function.

[@user-vq5nz6yk1h]

What about whitehead and russell? I guess they came up with such an idea way earlier... And the problem with a constructibility is that very important theorems couldn't be proven f.e. that every vectorspace has a basis or if you like non-standard analysis or even normal analysis you would loose many theorems that are quite crucial.

[@Luxcium]

I did not find the other part of the video on numberphile maybe someone can pass me the link

[@mzg147]

For me, it always been that the sign ∩ was turned 90 degrees anticlockwise in this statement. :)

[@karlkastor]

I actually once used 2 (element) 3 in a Discrete Maths homework where we couldn't use

[@matthewmann8969]

Computers along with there parts be it Monitors, Screens, Keyboards, Mouses, Remotes, Modems, Scanners, Printers, Floppy Discs, SD Cards, CPU's, and other devices can go hand in hand whether they are desktops, laptops, I pads, kindles, smart phones, cell phones, palm pilots, and other electronic devices and can serve well if they do not over heat or run out of storage space.

[@MrAyokunle01]

isn't Formal Programming a way of proofing mathematical theorems?

[@jeongheonlee4556]

I was watching with subtitle, and i saw he was gonna have to pronounce Coq, and couldnt wait to hear that.

[@SSJHF]

Dr Thorsten Altenkirch At 13:50, you talk about the Univalence Principal, where it is stated that if two things are equivalent, then they are equal. I have interpreted this as "If two things are logically equivalent, then they have the same properties. I shall show by example that this is not always the case: From the premises "forall x (Sx implies Px)", it can be proved that "Exists x (Sx & Px) iff Exists x(Sx) Using this example, I shall prove that if two logical expressions are equivalent, they don't necessarily have the same properties. In this example the property they don't have in common will be truth value. Take both Sx and Px to be "x=x". Substitution gives (1): "forall x (x=x implies x=x)" can prove "Exists x (x=x and x=x) iff Exists x (x=x)" (1) However, by the principal of transposition, it will also be true that (2): "forall x (not (x=x) implies (not x=x))" can prove "Exists x (not x=x) and (not x=x)) iff Exists x (not x=x)" (2) Example (1) has a truth value of true, however that of (2) is false. (x=x is always true, likewise (not x=x) is always false.) Thus if two statements are logically equivalent, they do not always have the same properties. Using transposition again, this means that if two statements have the same properties, they are not always the same statement.

[@ThorstenAltenkirch]

I didn't mean "logical equivalence" but logical equivalence is a special case. Indeed all operations on propositions in type theory are "truth functional". I don't understand your counterexample in particular I don't know what the principle of transposition is. I have no idea how you justify the step form (1) to (2).

[@SSJHF]

It turns out I made a mistake in the proof. I found out that I had used a universal specification rule on a negated universal statement. Because it was negated it was existentially quantified and the rule couldn't be used. Sorry about that. (Thanks for the reply though)

[@ThorstenAltenkirch]

Alex Armstrong no problem. And cheers to you for experimenting and dis overnight your own flaw.

[@zubmit700]

Thanks! Very interesting.

[@dominiquegibeau2856]

This video is really abstract to me compared to the other. In some videos the most basic concepts (to me) are explained but this one is really hard to follow, so much stuff is considered to be known and there doesn't seem to be much concrete stuff to relate to. It would have helped if it had been a bit more scripted, may be with examples or something. It's quite hard to get into Dr Thorsten Altenkirch's head for this topic!

[@user-tx4wj7qk4t]

The entire topic is abstract and you'd basically be learning math from scratch to understand it.

[@prathameshausekar]

Can anybody relate this with typescript, babel and how types(shapes) are identified and are considered to be interpreted into another types. Like replacing a type instance with another equivalent instance which do the work.

[@Arthur0000100]

How would you check the infinitude of number of primes via computing??

[@0lifinz]

can someone explain what this math on the whiteboard behind him is about?

[@kovacsandras]

It's about his research for formalizing type theory inside type theory. Basically, if lots of math can be expressed in TT, why not try TT itself as well? Since proofs in TT are executable programs, modeling TT inside TT is also a way of doing metaprogramming and proving properties of metaprograms in the same system.

[@anttikarttunen1126]

Until a latter day Gödel arrives. (this is a reply to András Kovács's comment below).

[@todmann67]

More of this!

[@astroid-ws4py]

Nice explantions but I doubt many will understand, I learned Measure Theory and thus can understand the general outline but those unfamiliar will be lost.

[@shamrockfrost1856]

This makes me feel guilty about not having read TAPL for two weeks...

[@aperson4051]

I will die a happy man when the producers of James Bond finally hire this man to be their evil genius.

[@vincentkubicki1626]

Spelling out a rational plan that works in the end :)

[@snippletrap]

2 as an element of 3 doesn't seem silly to me.

[@arnetrautmann9783]

A function that does not function should not be called a "function". Makes sense on so many levels!

[@dukeradwardthe5th843]

Is there a technical limitation for the 50fps?

[@RalphInRalphWorld]

Brix Zigelstein It's because they're Britons and they grew up with PAL.

[@KuraIthys]

Brix Zigelstein Yes, it's PAL equipment, and also reduces the risk of light flickering effects when filming in areas with 50 hz mains power.

[@reactiveland3111]

Where does category theory sit here in relation to type theory and rest?

[@johnjordan3552]

11:32 "It's true that 2 is an element of 3, doesn't really make any sense, right?" I mean, isn't 3 basically == | | | And 2 == | | so there indeed is a *| |* inside 3. So 2 is indeed an element of the set called 3

[@ConnorwithanO]

So would Type Theory make it possible to compile abstract math into executable code? I ask because that is basically what I dream about.

[@kovacsandras]

Yes.

[@ConnorwithanO]

Cool!

[@FalconGames109]

Kind of... although in general when you compile type theory it's more along the lines of interpreting it. For example, for a Coq proof to be "proven," all you have to do is compile it and there's nothing left to execute. So in a sense, executing the abstract math happens as your proof gets verified. As a result, it doesn't feature many tools for writing executable code (although it does allow you to "extract" the code into another language that can provide the tools for writing useful programs). You can also use some other languages to compile type theory programs into executable programs (Idris and ATS, for example).

[@xybersurfer]

no. you would have to create a proof to have a program (proofs are programs). and proving in Coq is much harder than conventional programming

[@user-vf8ti4dq3d]

this guy is my spirit animal

[@BlackHermit]

I'm a Swedish mathematician as well.

[@SubhomoyHaldar]

6:43 "Dysfunctional function". LOL

[@RandallStephens397]

Is it wrong that I love the sound of this man's voice more than what he's talking about?

[@amberstiefel9748]

Type vs set transcends "has a" and "is a" (in no particular order but maybe I'm off target..?)

[@guy12343456]

Is Computer Science consider a subfiled of Mathematics? It has its origins rooted in Set Theory, Graph Theory, and other mathematical fields, so wouldn't it be redundant to say "Computer Science union Math" when describing Type Theory?

[@guy12343456]

My bad, "Computer Science intersection Math"

[@binarycat1237]

computer science is applied maths

[@Vulcapyro]

There are subjects in Computer Science unrelated to Mathematics. There are subjects in Mathematics unrelated to Computer Science. The symmetric difference is going to be nonempty.

[@htmlguy88]

+Vulcapyro like ?

[@JohnDoe-qx3zs]

+htmlguy88 Computer science includes a lot of subjects related to the physical and practical aspects of computing, such as real world efficiency, caching, representation of human language text, issues with human-machine interaction, making the work less error prone etc. Mathematics includes subjects that cannot be accurately represented in computers, such as infinitely precise numbers, infinitely large sets, the entire field of mathematical analysis (differential and integral calculus) etc.

[@StankyPickle1]

"A function that does not function should not be called a function" -- Made me laugh, but has a very concrete truth to it.

[@LucasTreffenstadt]

ja

[@Elastane]

1:43 He may be clever but dirty sounding names are the basis of 91% of all British humour :D

[@meinsouza]

ja?....ja?....ja?

[@SHUBHAMGI]

Marcelo Souza what does that mean?

[@garetclaborn]

@marcelo ja @saber it means "ya"

[@pid8307]

Did I get this correctly? - Set theory is like a declarative programming language and a set may not be enumerable or infinite (termination problem); - Type theory is more constructive much like an imperative programming language.

[@XetXetable]

No, if anything, it's the opposite, as type theories tend to be functional languages. Set theory isn't like programming at all. It's a completely static logical system which, by default, has no computational interpretation. Type theory exists so that a computer can internalize the semantics of what a program is meant to do. If you want a program to sort a list, you can use type theory to define what it means to sort a list, then a type checker verifies that the program meets that specification within that type. What's significant is that, at the extreme ends of expressiveness, this is sufficient to act as a foundation for mathematics.

[@Cd4sh]

Computer Science ∩ Mathematics = Computer Science

[@m13m]

What are the axiom of mathematics which can be used to derive entire mathematics?

[@Kram1032]

there isn't just one set of axioms you can use and how you choose changes what you can show.

[@matekon2]

Kram1032 the most popular i would say are the zermelo fraenkel axioms, which are essentially rules you can follow to built sets

[@m13m]

Kram1032 it's weird that i was playing with lean yesterday.

[@IchBinKeinBaum]

While there are several sets of axioms which you can use as base for most of your math there is actually no set of axioms which - you can derive all maths from - is complete (i.e. every true statement can be proven to be true), and - is free of contradictions (i.e. no statement can be proven true and false). This is known as Gödel's incompleteness theorem.

[@davidwuhrer6704]

The Peano axioms mentioned in the video are probably the easiest to get started with. However, mathematics wouldn't be what it is if you could not devise your own systems. Bill Gosper famously delivered a proof about polynomial division just by optimising working code. Besides, mathematics is proven to never be complete. Deriving its entirety is an absurd idea. Some things are simply true, even though they cannot be constructed. DeMorgan's rules, for example, are proven true by exhaustion, but are not deduced. And some things are neither true nor false. And there is proven to be no end to such things, no matter how many you define axiomatically.

[@danielescotece7144]

Peano arithmetic is a way of defining natural numbers via induction, I don't understand how it can be use to encode the natural set.

[@jpratt8676]

Daniele Scotece Pretty sure what he means is that you represent the natural numbers as the set of things that can be produced from peano's successor function and 0. I.e. {0, 0+1, 0+1+1...}. So you define the set by induction. Not sure how to use that efficiently but there's probably some very smart maths for doing it.

[@danielescotece7144]

Oh I see that now, thanks sir, always a pleasure to see thoughtful comments on yt! Have a nice day