Pi, Recursion, and the Deprecated Type Languages

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