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: Coding Machines

Story: Coding Machines

What if the tools you trust were actually betraying you? Join us for a riveting story where a team of software developers discovers that their compiler is compromised. What starts as suspicion of a si...

3 Mai 202448min

Story: Code, Kickflips and Crunch Time - Mick West's Neversoft Journey

Story: Code, Kickflips and Crunch Time - Mick West's Neversoft Journey

Meet Mick West, whose career began in an unusual office setup — sandwiched between a kebab shop and a phone sex hotline. From there he worked all over Manchester, making computer games for Tiertex and...

2 Apr 202457min

Story: Leaving LinkedIn - Choosing Engineering Excellence Over Expediency

Story: Leaving LinkedIn - Choosing Engineering Excellence Over Expediency

What if your dedication to doing things right clashed with your company's fast pace? Chris Krycho faced this very question at LinkedIn. His journey was marked by challenges: from the nuances of remote...

4 Mar 202447min

Story: Beautiful Code - Inside Greg Wilson's Vision for Software Design

Story: Beautiful Code - Inside Greg Wilson's Vision for Software Design

Greg Wilson has been on a decades-long quest to transform how we teach and talk about software design. From getting rejections for using the term "beautiful code," to empowering scientists through wor...

2 Feb 202457min

Story - Code as a Lifeline: Brain Injury Sparks Python Mastery

Story - Code as a Lifeline: Brain Injury Sparks Python Mastery

What if your dreams were suddenly ripped away? What if your talents vanished, your passions erased? That's what happened to Jason McDonald when a traumatic brain injury at 16 ravaged his planned desti...

2 Jan 202444min

Story - From 486 to Vue.js: Evan You's Full-Time Gamble on Open Source

Story - From 486 to Vue.js: Evan You's Full-Time Gamble on Open Source

From the early days of exploring creative possibilities on a 486 computer in his childhood to developing one of today's most popular web frameworks, Evan You's journey is a tale of passion and innovat...

4 Des 202346min

Story: Platform Takes The Pain

Story: Platform Takes The Pain

How did Spotify scale from 10 engineers to 100s to 1000s ...without slowing down? Without becoming corporate?  Facing an IPO deadline, Pia Nilsson worked with 300 teams to transform how Spotify built ...

2 Nov 202348min

Story: Sloot Digital Coding System

Story: Sloot Digital Coding System

Lost treasure. Conspiracy theories. Impossible tech demos.  Jan Sloot claimed to have invented revolutionary data compression that could fit a full movie into a tiny smart card chip. Top executives an...

2 Okt 202351min

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