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: 2020 Year End

Welcome to the year-end episode. Today is all the bonus questions. Often times I have questions that I want to ask guests, but they don't quite fit the overall theme of the episode. So today we're goi...

1 Tammi 202134min

Story: Frontiers of Performance with Daniel Lemire

Did you ever meet somebody who seemed a little bit different than the rest of the world? Maybe they question things that others wouldn't question or said things that others would never say. Daniel i...

1 Joulu 202047min

Story: The Birth of Unix with Brian Kernighan

As Brian Kernighan said "UNIX since the start has become a vehicle for creating and using programming languages." Brian initiated work on what would become the UNIX system. He helped develop it to run...

1 Marras 202051min

Story: To The Assembly

How do CPUs work? How do compilers work? How does high-level code get translated into machine code? Today's guest is Matt Godbolt and he knows the answers to these questions. How he became an expert i...

1 Loka 202041min

Story: Memento Mori

Preparing our minds for the inevitable - death is pressing. After facing terminal cancer, Kate Gregory reminded herself that this event can still become inspiring by focusing on the positive. In this ...

1 Syys 202040min

Story: We are teaching Functional Programming Wrong

Today Richard Feldman shares his story of going from javascript developer to elm developer to functional programming teacher. Along the way, Richard finds that people are teaching functional programm...

3 Elo 202046min

Story: Software That Doesn't Suck With Jim Blandy

Building Subversion Software is just the tool and it should get out of your way. In this episode, we will discuss Jim Blandy's insights on how to build and recognize improvements for a great developer...

1 Heinä 202037min

Story: Unproven Tech Case Study with Sean Allen

Choosing The Right Tool For the Job Choosing the right programming language or framework for a project can be key to the success of the project. In today's episode, Sean Allen Sean shares a story of p...

10 Kesä 202039min