Please log in to watch this conference skillscast.
It so happens that functional languages can be used as theorem provers, by virtue of the so-called Curry-Howard correspondence. Besides its theoretical significance, there is an appealing practical corollary: using logic exercises and recreational puzzles to improve our mastery of our language of choice, Scala. This talk has precisely the goal of explaining type-driven development and basic features of the Scala 3 type system, using Aristotle’s syllogisms, Raymond Smullyan’s Knights and knaves puzzles, and common propositional tautologies. In particular, we will see how signatures built upon algebraic data types and dependent types allow us to model these logical problems, and how type-driven development mimics the logical reasoning used to find the corresponding proofs.
YOU MAY ALSO LIKE:
- Scala Days 2023 (Online Conference on 1st - 30th December 2023)
- Hack & Hang Night (in Chicago on 21st March 2023)
- Think Functionally (Online Meetup on 23rd March 2023)
- Teaching Haskell...To High Schoolers! (SkillsCast recorded in December 2022)
- Teaching Haskell...To High Schoolers! (SkillsCast recorded in December 2022)
What Logic can Teach Us, Scala Programmers
Juan M. Serrano
CTO & Co-Founder, Habla Computing