CoRecursive: Coding Stories1 Joulu 2018

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

Tämä jakso on lisätty Podme-palveluun avoimen RSS-syötteen kautta eikä se ole Podmen omaa tuotantoa. Siksi jakso saattaa sisältää mainontaa.

Jaksot(115)

Chat: Quines, Polygot Code, and Other Fun Computations

Today, previous guest and my neighbor Don Mckay and I will discuss items from the endless fascinating Cursed Computer Iceberg Meme. The Iceberg is a giant list of "the peculiarities and weirdness of c...

2 Syys 20211h 1min

Story: Full-Time Open Source

Today's show: How to Quit Your Job and Work on Open Source Full Time. This story has it all, balancing open source work and full-time employment, building up enough supporters and enough savings to l...

2 Elo 202146min

Story: The Untold Story of SQLite

On today's show, I'm talking to Richard Hipp about surviving becoming core infrastructure for the world. SQLite is everywhere. It's in your web browser, it's in your phone, it's probably in your car, ...

2 Heinä 202138min

Story: From Competitive Programming to APL

Today on the show, we have solving algorithmic programming problems. You know when you interview for a job to write CSS and they ask you to reverse a binary tree on the whiteboard using C and in const...

2 Kesä 202153min

Story: Ethereum Rescue

Today I talk to Dan Robinson about trying to get someone their money back on Ethereum. He's going to be battling this murky world of blockchain high-frequency bots. Along the way, we'll learn how trad...

2 Touko 202134min

Story: Apple 2001

David Shayer worked at Apple for 14 years, and he has a wild experience to share. Apple has a unique culture, and David will give us an insider view of what it was like for him at Apple during the 200...

3 Huhti 202148min

Story: Video Game Programming From Scratch

I'm not really a big gamer, but lately, I've fallen down this rabbit hole into the world of Casey Muratori, and this project that he started on Twitch in 2014. He is building a video game from scratch...

1 Maalis 202141min

Story: Reinforcement Learning At Facebook with Jason Gauci

If you ever wanted to learn about machine learning you could do worse than have Jason Gauci teach you. Jason has worked on YouTube recommendations. He was an early contributor to TensorFlow the open-s...

1 Helmi 202138min