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

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

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

Denne episoden er hentet fra en åpen RSS-feed og er ikke publisert av Podme. Den kan derfor inneholde annonser.

Episoder(115)

Story: LISP in Space

Story: LISP in Space

Have you ever had a unique approach to a problem and been excited to use it, but you're met with skepticism?   Today's story: what happens if you take someone who's passionate about LISP and put them ...

2 Mai 202238min

Chat: April Fools' Is Cancelled

Chat: April Fools' Is Cancelled

On this day in 2014 "lame april fools' jokes" were banned from hacker news.    Today in our first This-Day-in-History segment, I want to share some of history not just of April Fools', but of tech pra...

1 Apr 202238min

Story: The Story Graph with Nadia Odunayo

Story: The Story Graph with Nadia Odunayo

Whenever I work on a side project, I can't help but daydream of it taking off in a big way. For today's guests, something like that did happen.    When Nadia started building her side project, she did...

2 Mar 202248min

Story: Serenity OS

Story: Serenity OS

How would you build an operating system?     My answer is I wouldn't. First off, I don't know how. And the second thing is it seems like to large of a task. It took thousands of developers to build Wi...

1 Feb 202241min

Chat: The Internet Is Made of Duct Tape

Chat: The Internet Is Made of Duct Tape

Today, I have two of my favorite guests together: Krystal Maughan and Don McKay. We are going to be sharing strange and interesting facts about computing. I'm super pumped about this because, sometime...

2 Jan 202242min

Story: Cocoa Culture

Story: Cocoa Culture

The last episode, I said I wasn't sure there was such a thing as culture, but that's not the case. Every place I've worked has been a bit different, and often those differences had huge impacts on the...

2 Des 202144min

Story: Leaving Debian

Story: Leaving Debian

Today's story is an insider view of Debian. One of the oldest Linux distributions and probably one of the longest-running volunteer-based open-source projects. Joey Hess is my guest, and he dedicated ...

2 Nov 202140min

Story: The Original Remote Developer

Story: The Original Remote Developer

Today's episode is about remote work. Well, sort of. I found someone with a different perspective on remote work and a fantastic story to share, Paul Lutus. I think that he might be the original remo...

4 Okt 202141min

Populært innen Politikk og nyheter

giver-og-gjengen-vg
aftenpodden
forklart
aftenpodden-usa
stopp-verden
popradet
fotballpodden-2
lydartikler-fra-aftenposten
rss-gukild-johaug
det-store-bildet
dine-penger-pengeradet
nokon-ma-ga
rss-ness
hanna-de-heldige
rss-espen-lee-usensurert
aftenbla-bla
grasoner-den-nye-kalde-krigen
rss-dannet-uten-piano
e24-podden
rss-penger-polser-og-politikk