SkillsCast

What Logic can Teach Us, Scala Programmers

software-development puzzles types logic scala-3

4th October 2022 in Online Event

There are 23 other SkillsCasts available from ScalaCon 2022

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:

Thank you to our sponsors and partners

Platinum

Gold

Silver

Bronze

Partners

About the Speaker