What are dependent types? aka the Calculus of Construction (as a type wizard)

An almost baked video, but now enhanced.
Examples shown:
github.com/EduardoRFS/youtube...
Yes yes ... wikipedia
en.wikipedia.org/wiki/Calculu...
Social media stuff:
/ eduardorfs
/ theeduardorfs

[@CodeTalker23]

this guy disappears and then comes back with a banger (btw we need books about these topics to read further)

[@EduardoRFS]

Just because you asked boss. Types and Programming Languages Advanced Topics in Types and Programming Languages Both by Pierce.

[@twenty-fifth420]

I decided for my dream programming language I want dependent types. This video helped me understand further, corrected misunderstandings and made me re-evaluate my perspective. Thank you! Do you have free resources on Coq? The fact it was made in OCaml makes me want to write my language in OCaml but neither her nor there. 😂

[@bernardoborges8598]

Have you ever tried Lean Prover?

[@yessure5792]

good content, thank you

[@kallekula84]

Which VSCode plugin do you used that gives you inline error messages?

[@insertoyouroemail]

Cool! I'm just a Lisper but I've been thinking about how I could introduce types to my programs.

[@reycorbie3581]

the little typer/prover

[@insertoyouroemail]

@@reycorbie3581 Got both of them! :)

[@samuelfreitas5793]

Doskya

[@rastrian]

First