Tech Talk: The Little Typer With Daniel Friedman and David Thrane Christiansen

Tech Talk: The Little Typer With Daniel Friedman and David Thrane Christiansen

Author: Adam Gordon Bell - Software Developer December 1, 2018 Duration: 1:07:27

Tech Talks are in-depth technical discussions.

When it comes to type systems "I am, so far, only in the dependent types camp" - Daniel P. Friedman

You can write more correct software and even rigorous mathematical proofs.  Prepare for some mind stretching.

Previous guests like Edwin Brady and Stephanie Weirich have discussed some of the exciting things a dependent type system can do Miles Sabin said dependent types are surely the future. This interview is to get us ready for the future.

Daniel P. Friedman is famous for his "Little" series of books. Little Schemer, Little prover, Little MLer and so on. These books are held in high regard.

Here is a quote from Doug Crockford:  "Little Schemer teaches one thing, a thing that is very difficult to teach, a thing that every profession programmer should know, and it does it really well. These are lessons that stick with you."
The latest one is the little typer and its about types. Specifically dependent types.

Dan's coauthor is David Thrane Christiansen, Idris contributor, and host of a podcast about type theory that is way over my head.

Together they are going to teach us how the programming skills we already have can be used to develop rigourus mathematical proofs.

Stay tuned to the end for my guide to working thru the book.

Originally published at CoRecursive here

Join Our Slack Community


In CoRecursive: Coding Stories, host Adam Gordon Bell sits down with software developers to explore the human narratives woven into the technology we build. This isn't a technical interview focused on syntax or best practices, but a deeper dive into the pivotal moments, creative struggles, and personal insights that shape how code comes to life. Each conversation reveals the context behind decisions, the stories of failure and breakthrough, and the often-overlooked human elements that define our craft. As a software developer himself, Adam guides these discussions with genuine curiosity, pulling out anecdotes and reflections you won't hear anywhere else. The podcast lives in the intersection of News, Education, and How-To, but through the lens of lived experience. You'll hear about the origins of influential projects, the rationale behind unconventional solutions, and the personal journeys that lead developers to their philosophies. Listening feels like pulling up a chair with thoughtful peers, offering a richer understanding of the profession that goes far beyond the screen. This is where the abstract becomes concrete, through the stories and people behind the code.
Author: Language: English Episodes: 100

CoRecursive: Coding Stories
Podcast Episodes
Story: The Aging Programmer [not-audio_url] [/not-audio_url]

Duration: 41:52
Kate Gregory has been writing C++ for over forty years. Books, keynotes, a consulting firm she built from the ground up. At sixty-three, she's one of the most experienced programmers alive. She surveyed hundreds of softw…
From Hacker News to TikTok - How Algorithms Learned to Hook Us [not-audio_url] [/not-audio_url]

Duration: 41:32
Corey told me about his AI cat reel problem. He found these AI-genearted cat videos hilarious. Who makes these? He kept sending them to his wife. Then he tried to stop watching and he couldn't. So I went down the rabbit…
Notes: The Universal Paperclip Clicker [not-audio_url] [/not-audio_url]

Duration: 11:05
Multiple VS Code windows. "Agent stopping" in a robot voice. A laptop stand on the treadmill so Claude can keep working while I run. The Big Rich sitting unread by the fireplace while I check if the migration's done. Som…
Story: Godbolt's Rule - When Abstractions Fail [not-audio_url] [/not-audio_url]

Duration: 44:13
What do you do when your code breaks and the only fix is to dig into the runtime below? Matt Godbolt lives for that. Tile-based renderers, color-coded scanlines, zero-copy NICs—each story is a clue that leads past the ab…
Quick Update [not-audio_url] [/not-audio_url]

Duration: 8:52
A quick update from Adam about the podcast's current state, consistency challenges, and what's coming next. Episode Page Support The Show Subscribe To The Podcast Join The Newsletter
Coding in the Red-Queen Era [not-audio_url] [/not-audio_url]

Duration: 42:24
What do we risk when we let AI do the heavy lifting in our coding? Are we giving up the thinking that makes us good at what we do? And as expectations keep rising to match productivy gains, is all this speed really helpi…
When AI Codes, What's Left for me? [not-audio_url] [/not-audio_url]

Duration: 39:51
I've always found meaning—and a lot of strength—in building things. Now, with AI coding agents changing the way we work, it's easy to feel threatened, like something essential might get taken away. But honestly, that cre…