What logic can teach us, Scala programmers

on YouTube ↗52m

" summary

Uses Scala 3 to encode propositions as types and proofs as programs, implementing examples from propositional logic, Aristotle syllogisms and Smullyan knights-and-knaves. Demonstrates mechanical type-driven development: lambda introduction, pattern-match destructors, hole-filling that produces code which compiles. Shows when proofs fail intuitionistically (need law of excluded middle to recover classical tautologies), models predicates with path-dependent types and universals with dependent function types, and provides a working repo with implementations for 24 Aristotle syllogisms.

AI-written summary · about

" chapters (6)

1. 0:00Introduction to logic and Scala
2. 1:52Propositional logic in Scala
3. 21:14First-order logic with syllogisms
4. 35:58Second-order logic puzzles
5. 47:16Lessons and takeaways
6. 51:10Resources and conclusion

" related talks

• 37mIn Types We TrustBill Venners · Scale By The Bay 2019
• 01h 34mFormal Logic UndressedPaul Snively · Scala World 2015
• 44mIn Types We TrustBill Venners · Scala Days Lausanne 2019
• 23mReasoning about types and codeSergei Winitzki · Scale By The Bay 2019
• 41mThe Dialectics of Type-Level ProgrammingAaron Levin · Lambda World 2016
• 01h 01mLearning Propositional Logic with Logic ProgrammingJimmy Torre · LambdaConf 2018
• 56mCalculating Intuitionistic Logic in ScalaVlad Patryshev · LambdaConf 2019
• 15mLogic Programming with Extensible Types (Lightning talk)Ivan Perez, Ángel Herranz, Julio Mariño · PADL 2025