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:
- Haskell at Work (Online Workshop on 30th January - 2nd February 2023)
- YOW! December 2022: Online (Online Conference on 5th - 13th December 2022)
- YOW! Brisbane Developer Conference 2022 (in Brisbane on 5th - 6th December 2022)
- London Java Community Unconference (in London on 5th December 2022)
- Next generation i18n with rust (icu4x) and zero-copy deserialization (in Zürich on 7th December 2022)
- Taming the Context Beast (SkillsCast recorded in October 2022)
- The Middle Way for Static Typing in Spark DataFrames (SkillsCast recorded in October 2022)