Learn from software development experts. Hosted by Adam Gordon Bell
God’s Programming Language With Philip Wadler
Does god code in Haskell?
Professor and accomplished programming language researcher Philip Wadler believes that typed lambda calculus was discovered not invented — part of the underpinnings of the universe itself. As a result, functional programming languages are more fundamental and deeply justified than their alternatives.
We talk about this principle, which has guided his career. Phil takes us through the history of computer science from Turing to Alonzo Church. Eventually we get to what the movie Independence Day got wrong and what language a theoretical creator deity would program in.
Show notes:
TIME JUMP
- 01:49 - Programming Languages are absolute
- 03:18 - Computer Science is a horrible name
- 04:37 - What is computation?
- 06:01 - Lambda Calculus
- 07:00 - Women were the first computers
- 12:24 - Gödel, undecidability and the halting problem
- 18:42 - Types existed before computers
- 26:49 - Adjacent Possible
- 28:51 - Invention vs Discovery
- 36:05 - Logicians and the fundamental nature of the universe
- 37:29 - God's Programming Language
- 40:08 - Aliens computer viruses
- 45:07 - Omniversal Programming Languages
- 47:48 - Generics are innate
- 50:53 - Logicians first
- 56:00 - Bringing Monads to haskell
- 58:44 - The secret to good research
Leave a Comment
Subscribe In Itunes!
- Burn out and Recreational Coding with Jamis Buck
January 25, 2019
62 min - Software as a Reflection of Values With Bryan CantrillDecember 18, 201879 min
- The Little Typer With Dan Friedman and David ChristiansenDecember 1, 201867 min
- Big Ball Of Mud – Architecture and Services with Wade WaldronNovember 14, 201860 min
- God’s Programming Language With Philip WadlerOctober 22, 201860 min
- Concurrency and FP with Riccardo TerrellOctober 3, 201862 min
- Test in Production with Charity MajorsAugust 31, 201847 min
- Domain Driven Design and Micro Services With Vaughn VernonAugust 17, 201849 min
- Http4s With Ross BakerJuly 27, 201850 min
- Moves and Borrowing In Rust With Jim BlandyJuly 3, 201864 min
- Dependent Types in Haskell with Stephanie WeirichJune 13, 201858 min
- Micro Service Architectures With Jan MachacekJune 6, 201866 min
- Rust And Bitter C++ Developers With Jim BlandyMay 16, 201862 min
- Erlang And Distributed Systems with Steven ProctorMay 2, 201866 min
- Graphql And Sangria With Oleg IlyenkoApril 18, 201855 min
- Purescript And Avocados with Justin WooApril 4, 201851 min
- Throw Away the Irrelevant with John A De GoesMarch 21, 201868 min
- Generic Programming and Shapeless with Miles SabinMarch 7, 201860 min
- Total Programming Using Swift with Andre VidelaFebruary 12, 201853 min
- Type Driven Development and Idris With Edwin BradyJanuary 29, 201859 min
- Algebraic Domain Modelling using Functions With Debashish GhoshJanuary 22, 201858 min
- Design Principles From Functional Programming with Runar BjarnasonJanuary 10, 201851 min
- Scala at Duolingo with Andre Kenji HorieJanuary 7, 201853 min
- Incident Response with Emil StolarskyJanuary 5, 201851 min
- Scala Native with Denys ShabalinJanuary 1, 201848 min
Habib Alamin
I’d really like a source on the claim that men basically kicked women out of computing when they figured out it was interesting work, because it sounds like an absurd claim — and I’m really not paraphrasing that much; listen from 7 minutes in if you don’t believe me — and it’s pushing an agenda.
Adam Gordon Bell
It sounded to me like Phil source was someone whom actually experienced this, a friends mother. It doesn’t seem like an absurd claim to me.
Habib Alamin
I’m talking about a source that can be corroborated, perhaps replicated (maybe a study), or somehow fact-checked in one way or another.
The personal experience of someone I don’t know and their perspective on that personal experience is not a credible source. There are a lot of things that someone could mean when they say they were being pushed out before we even get into its validity — anything from “women began to be blacklisted from every place that did computing” to, “so many men started coming in that the ratio of women started decreasing precipitously”.
It sounded to me like Phil’s source was more than just his friend’s mother, anyway; Phil referred to “other historical documents describing that” which he found after his friend’s mother said this to him. I would like to know which historical documents he’s talking about.
Chris
A quick Google has only killed a couple people. This paper from the ACM, see the section titled “The First Machines”: https://courses.cs.washington.edu/courses/csep590/06au/readings/p175-gurer.pdf
This article from NPR touches on the overall trend as well: https://www.npr.org/sections/alltechconsidered/2014/10/06/345799830/the-forgotten-female-programmers-who-created-modern-tech
This article in wikipedia is also well-cited so any of those sources might also help. https://en.wikipedia.org/wiki/Women_in_computing#1940s
Habib Alamin
I was asking specifically about Philip Wadler’s sources, not Google search results.
That said, thank you for these links. I will go through them when I get a chance.
Habib Alamin
None of these sources talk about men “pushing” women out, much less as they “figured out” that it was interesting work. It looks less like men pushed women out when they figured out computing was interesting work and more like higher numbers of men started joining the field as it actually started changing.
In other words, more men started joining as it actually _became_ more interesting (less repetitive mathematical calculation work, more career instead of job) and as it started being more lucrative, too. The end of male conscription also surely had an impact.
Tangled Z
Mar Hicks has recently released a book on this: Programmed Inequality: How Britain Discarded Women Technologists and Lost Its Edge in Computing .
Habib Alamin
Thanks. What did you think of it (assuming you read it)?
haisheng
what was the paper Philip said “very readable and entertaining” by Russell?
Tom
I think this is Russell’s paper that was referenced in the podcast; it introduces the theory of types and Philip Wadler mentioned it is an example of a very readable paper: [Mathematical Logic as Based on the Theory of Types](https://fi.ort.edu.uy/innovaportal/file/20124/1/37-russell1905.pdf)