Philip Wadler discusses the deep connection between logic and programming, revealing how every program corresponds to a proof. The podcast explores historical models of computation, Godel's influence, and challenges in defining calculable processes. It also delves into lambda calculus, Turing machines, comedy in programming, and the evolution of computing from military funding to logical systems.
Lambda calculus and Turing machines provide equivalent models of computation, highlighting the unity of different approaches to calculability.
Establishing a connection between logic and programming reveals how logical operations map to programming constructs, offering insights into the intersection of types and logic.
Dependent types in programming, influenced by logical quantifiers, demonstrate the synergy between logical reasoning and program design, enhancing software development practices.
Advanced type systems like Idris enable programmers to create rigorous proofs, ensuring program correctness and deepening the understanding of logical structures in software development.
Deep dives
Lambda Calculus and Turing Machines: They Both Have a Halting Problem
Lambda calculus and Turing machines, developed by Church and Turing, respectively, in the 1930s, provide different ways to explore effectively calculable functions. Both encounter a halting problem where certain programs cannot determine whether they halt, showcasing the inherent complexities of computation.
Georg Kreisel on Types and Logic: A Fundamental Connection
Georg Kreisel's work in logic led to a significant breakthrough with the introduction and elimination rules, providing a formal system that clarified logical formulas. This system established a profound link between logic and programming, demonstrating that conjunction, disjunction, and implication in logic correspond to Cartesian products, disjoint sums, and functions in programming, offering a fresh perspective on the intersection of types and logic.
Dependent Types: Bridging Logic and Programming in a Clever Way
Curry and Howard's 1969 paper showcased the correspondence between logical operations and programming constructs, specifically illustrating that logic's existential and universal quantifiers translate to dependent types in programming. This revelation established a bridge between logical reasoning and programmatic constructs, showcasing the power of dependent typing in software development.
Applying Logic in Programming: From Boolean Operations to Dependent Typing
Translating logical concepts to programming practices allows for innovative applications, such as performing Boolean operations on geometric primitives. This analogy provides a tangible way to grasp complex logical ideas and clearly illustrates the transformative impact of logic in the realm of software development.
The Power of Types in Programming
Types in programming, specifically demonstrated through examples like the factorial 5 equals 120 type, offer a powerful means of ensuring correctness at compile time. By leveraging advanced type systems like Idris, programmers can create watertight proofs and have a deeper understanding of their programs' logic structures. While such advanced type systems may seem daunting, they provide a structured way to enforce program correctness and facilitate a deeper exploration of logical concepts within software development.
Challenges of Logic and Proof Systems
Delving into concepts like intuitionistic logic and the law of excluded middle, the discussion highlights the intricate and occasionally contentious nature of proof systems. Ideas like rejecting the law of excluded middle challenge traditional notions of truth and falsehood, prompting a reconsideration of fundamental logical principles. Despite the complexities involved, exploring such concepts sheds light on broader applications in programming and underscores the importance of understanding logic in various contexts.
Balancing Theoretical Foundations with Practical Implementations
The podcast discussion underscores the need for harmonizing theoretical foundations, like bidirectional type checking and lambda calculus, with practical programming applications. While the theoretical underpinnings offer deep insights into logic systems and program structures, translating these concepts into tangible code implementations can be challenging. Bridging the gap between theory and practice, such as through accessible educational materials and simplified code demonstrations, can enhance understanding and encourage innovation in programming paradigms.
The subject of this episode's paper — Propositions as Types by Philip Wadler — is one of those grand ideas that makes you want to go stargazing. To stare out into space and just disassociate from your body and become one with the heavens. Everything — life, space, time, existence — all of it is a joke! A cosmic ribbing delivered by the laws of the universe or some higher power or, perhaps, higher order. Humanity waited two thousand years, from the time of the ancient Greeks through until the 1930s, for a means to answer questions of calculability, when three suddenly arrived all at once:
General recursive functions by Gödel in 1934, with functions of sets of natural numbers.
Lambda calculus by Alonzo Church in 1936, with anonymous single-variable functions.
Turing machines by Alan Turing in 1937, with a process for evaluating symbols on a tape.
Then it was discovered that these three models of computation were, in fact, perfectly equivalent. That any statement made in one could be made in the others. A striking coincidence, sure, but not without precedent. But then it was quietly determined (in 1934, again in 1969, and finally published in 1980) that computation itself is in a direct correspondence with logic. That every proposition in a given logic corresponds with a type in a given programming language, every proof corresponds with a program, and the simplification of the proof corresponds with the evaluation of the program.
The implications boggle the mind. How could this be so? Well, how could it be any other way? Why did it take so long to discover? What other discoveries like this are perched on the precipice of revelation?
Philip Wadler is here to walk us through this bit of history, suggest answers to some of these questions, and point us in a direction to search for more.
And we are here, dear listener, to level with you that a lot of this stuff is miserably hard to approach, presented with the symbols and language of formal logic that is so often inscrutable to outsiders. By walking you through Wadler's paper (and the much more approachable Strange Loop talk), and tying it in with the cultural context of modern functional programming, we hope you'll gain an appreciation for this remarkable, divine pun that sits beneath all of computation.
Cocoon is good. It's not, like, Inside or Limbo good, but it's good. Actually, just play Inside. Do that ASAP.
Hollow Knight, also extremely good. Can't wait for Silksong. But seriously, if you're reading this and have haven't played Inside, just skip this episode of the podcast and go play Inside. It's like 3 hours long and it's, like, transformatively great.
Chris Martens has done some cool work (eg) bringing together linear logic and games.
The Incredible Proof Machine is what some would call a "visual programming language" because proofs are programs. But it's actually really cool and fun to play with. Approach it like a puzzle game, and give it 10 minutes or so to get its hooks into you.
