CoRecursive: Coding Stories Tech Talk: The Little Typer With Daniel Friedman and David Thrane Christiansen
Dec 1, 2018
AI Snips
Chapters
Transcript
Episode notes
Understanding Dependent Types
- Dependent types can include ordinary programs within types to express more precise information.
- This enables types to describe properties like list length, increasing program correctness and expressiveness.
Origin of Little Schemer Style
- The Little Schemer book was created during an intense week-long session with students in 1973-74.
- It was collaboratively developed by walking to a blackboard and iterating ideas live, fostering an interactive teaching style.
Curry-Howard Correspondence Explained
- The Curry-Howard correspondence equates theorems with types and proofs with programs.
- Writing a program of a type effectively means proving the corresponding theorem, merging programming and logic.