Podcast appearances and mentions of edwin brady

Andres and Wouter interview Edwin Brady, most famous for his work on the Idris programming language. We talk about how he got interested in programming with dependent types, his thoughts on dependently typed programming in Haskell, and his vision for Idris.

I discuss dependent types, which are types that can contain non-type programs. An example of a dependent type is a list whose type contains its length. Instead of just writing List for a list that contains strings, dependent types include types like List that describe lists of exactly five strings. Dependent types can also be used to represent mathematics, in which case the programs that they describe count as proofs, and tools from programming can be used to write math. Dependent types used to be something that really required a research background, but there has been a lot of progress on making them more user-friendly and on writing accessible introductions lately. Languages mentioned: Idris is a self-hosted dependently typed language with type-level resource tracking Agda is a testbed for new ideas in dependently typed programming Lean 4 is a self-hosted dependently typed language that has a more conservative logical core than Idris or Agda, and attempts to appeal more to practicing mathematicians. Coq is a proof assistant based on dependent types that has been used to fully mathematically verify a C compiler Books mentioned: The Little Typer, by Daniel P. Friedman and David Thrane Christiansen is an intro to the core ideas of dependent types, in dialog form Type Driven Development with Idris by Edwin Brady, the creator of Idris, describes an approach to programming that uses expressive types as a way to make programmers' lives easier Programming Language Foundations in Agda by Phil Wadler, Wen Kokke, and Jeremy Siek describes the use of Agda for both programming and proving Software Foundations is a series of books that use Coq as an introduction to mathematically rigorous software development in a proof assistant. It's how I initially learned these topics!

As part of our interview series, we interviewed Edwin Brady, the creator of Idris, a dependently-typed programming language. In the interview, we discussed two of the programming languages Edwin has participated in the creation of: Whitespace and Idris. Edwin also shared some tips and tricks about language creation and talked about the future plans of the Idris language. This is an audio-only version of the interview. You can watch the original on our YouTube channel: https://www.youtube.com/watch?v=_prvbd0e_pI FP merch that doesn't suck: https://shop.serokell.io/ Read highlights on Serokell Blog: https://serokell.io/blog/from-whitespace-to-idris Follow on social media: https://twitter.com/edwinbrady https://twitter.com/serokell Learn more about us: https://serokell.io/ Contact us: academy@serokell.io

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

Edwin Brady is the creator of the Idris programming language and Author of the book Type-Driven Development with Idris and a computer science lecturer.  The book, the language and Edwin himself all seem to be chock full of ideas for improving the way computer programming is done, by applying ideas from programming language theory.   In this interview, we discuss dependent types, type holes, interactive and type-driven development, theorem provers, Curry–Howard correspondence, dependant haskell, total functional programming, British vs American spelling and much more.     Links: The Book Idris Lectures at OPLSS Idris Language Site

Edwin Brady speaks to Matthew Farwell about Type Driven Development and the Idris Programming language. The show covers: what a type is; static vs dynamic types in programming languages; dependent types; the Idris programming language; why Idris was created. Type safe printf modelling state in Idris modelling protocols in Idris modelling concurrency in Idris type driven development and how it changes the development process. Related […]

Edwin Brady speaks to Matthew Farwell about Type Driven Development and the Idris Programming language. The show covers: what a type is; static vs dynamic types in programming languages; dependent types; the Idris programming language; why Idris was created. Type safe printf modelling state in Idris modelling protocols in Idris modelling concurrency in Idris type driven development and how it changes the development process.

An unabridged version of the interview with Edwin Brady, the creator of Idris. Talking about the language itself, the concept of Dependent Types and the future of Type Systems. Code Podcast Forum: https://discuss.codepodcast.com/t/episode-5-type-systems/22 Episode produced by: Andrey Salomatin twitter.com/flpvsk Michael Beschastnov michael@codepodcast.com Guest: Edwin Brady twitter.com/edwinbrady ## Links Type-Driven Development with Idris https://tinyurl.com/typedd Idris Tutorial http://docs.idris-lang.org/en/latest/tutorial/index.html#tutorial-index LightYear – Parser Combinator for Idris https://github.com/ziman/lightyear Quantities – Type-safe physical computations and unit conversions in Idris https://github.com/timjb/quantities ## Music Mid-Air! @mid_air

Craig Stuntz talks about an Incredibly Strange Programming Language: Idris. Show notes: Craig's slides for Incredibly Strange Programming Languages Stir Trek conference The Sapir-Whorf hypothesis Type-Driven Development With Idris, by Edwin Brady TDD (Test Driven Development). If you've never heard of that, check out Kent Beck's seminal book, Test Driven Development: By Example. Improving Enterprises Papers We Love - Columbus Craig Stuntz's blog Craig Stuntz on Twitter Want to be on the next episode? You can! All you need is the willingness to talk about something technical. Theme music is "Crosscutting Concerns" by The Dirty Truckers, check out their music on Amazon or iTunes.

In this episode I talk with Edwin Brady. We talk Dependent Types and Idris. We cover his background of getting interested in dependent types, getting up and going with Idris, how to participate to drive Idris forward, and much more.

Guest speaker Edwin Brady talks about Idris in an extremely advanced podcast full of PhDs! Panel Edwin Brady Heinz Gies @heinz_gies Kevin Hammond @khstandrews Simon Thompson @thompson_si Zach Kessin @zkessin Conferences Elixir Conf EU April 23-24, Krakow http://www.elixirconf.eu/ PolyConf Krakow July 2-4 http://polyconf.com/ Erlang User Conference in Stockholm June 11-12 www.erlang-factory.com/euc2015 Code Mesh, London, November 2-4 http://lanyrd.com/2015/codemeshio/

In our second episode, we speak with Edwin Brady from the University of St. Andrews. Since 2008, Edwin has been working on Idris, a functional programming language with dependent types. This episode is very much about programming: we discuss the language Idris, its history, its implementation strategies, and plans for the future.