Tech Talk: Idris, Proofs and Haskell with Edwin Brady
CoRecursive: Coding Stories · Adam Gordon Bell
Audio is streamed directly from the publisher (traffic.libsyn.com) as published in their RSS feed. Play Podcasts does not host this file. Rights-holders can request removal through the copyright & takedown page.
Show Notes
Tech Talks are in-depth technical discussions.
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: