What Logic can Teach Us, Scala Programmers
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
What Logic can Teach Us, Scala Programmers
Juan M. Serrano
CTO & Co-Founder, Habla Computing