Podcasts about type driven development

Wouter Swierstra is a Math Bachelor's from the University of Utrecht, has done his PhD with Thorsten Altenkirch at the University of Nottingham, did a post-doc at Chalmers, has experience in the industry working on facilitating the design of embedded system using FP and currently is a Professor at the University of Utrecht and co-host of the Haskell Interlude Podcast. In this episode we talk about his trajectory into formal methods and functional programming. We talk about Datatypes a la Carte, the Expression Problem, Functional Pearls, Program Synthesis vs Program Calculation, and much more! 0:00 – Intro & Welcome 0:02:08 – Announcing the Type Theory Forall Merch Store! 1:12 – Early Influences: From Lenses to Logic 4:40 – Discovering Functional Programming in Utrecht 8:15 – On Monads, Papers, and Learning by Teaching 12:20 – What Makes a Paper ‘Beautiful'? 17:50 – PhD in Nottingham: Theory Meets Community 22:00 – Writing ‘Certified Programming with Dependent Types' 29:10 – Teaching Dependent Types: Challenges and Joys 34:00 – On Agda vs Coq: Philosophies and Use Cases 38:40 – Type-Driven Development in Practice 45:05 – The Power of Elegant Proofs 52:00 – Advice to Aspiring Researchers in Type Theory 1:03:00 – Beating C with Functional Programming 1:20:00 – Formal Verification and Loop Invariants 1:33:28 – Program Calculation vs Program Synthesis 1:39:00 – Formalizing Blockchain 2:01:38 – Final Thoughts Links Wouter Website Haskell Interlude Advanced FP Summer School ttforall twitch ttforall store Discount code for 10% off: typetheory

Dejan Miličić is an enthusiastic consultant and developer advocate at RavenDB with more than 20 years of experience as a professional software developer in designing, writing, and maintaining applications. Dejan is passionate about Open Source, RavenDB, Software Architecture, and Software Professionalism, supporting the Software Crafting Serbia community via workshops and meetups. He is an active proponent of knowledge sharing, professional ethics, and the usage of Type Driven Development and Functional techniques to reduce complexity, increase expressiveness, and improve the correctness of software. In his spare time, Dejan works on open-source projects, mentors startups in various development phases, and participates in Startup Accelerator programs supporting entrepreneurs through on-site and off-site consultations. You can follow Dejan on Social Media https://twitter.com/dejanmilicic https://www.linkedin.com/in/dejanmilicic/ PLEASE SUBSCRIBE TO THE PODCAST - Spotify: http://isaacl.dev/podcast-spotify - Apple Podcasts: http://isaacl.dev/podcast-apple - Google Podcasts: http://isaacl.dev/podcast-google - RSS: http://isaacl.dev/podcast-rss You can check out more episodes of Coffee and Open Source on https://www.coffeeandopensource.com/ Coffee and Open Source is hosted by Isaac Levin (https://twitter.com/isaacrlevin) --- Support this podcast: https://podcasters.spotify.com/pod/show/coffeandopensource/support

We talk with Louis Pilfold about how he created Gleam, a static typed language that runs on the BEAM. Louis explains some of the challenges with bringing static types to the BEAM and shares ideas on what can possibly be done about it. We learn how Gleam got started, how it works, and how Elixir and Erlang can interop with it. We cover the recently released Gleam OTP work, talk about Type Driven Development and much more! Show Notes online - https://thinkingelixir.com/podcast-episodes/023-gleam-and-static-types-with-louis-pilfold The post #023 Gleam and Static Types with Louis Pilfold appeared first on Thinking Elixir.

We talk with Louis Pilfold about how he created Gleam, a static typed language that runs on the BEAM. Louis explains some of the challenges with bringing static types to the BEAM and shares ideas on what can possibly be done about it. We learn how Gleam got started, how it works, and how Elixir and Erlang can interop with it. We cover the recently released Gleam OTP work, talk about Type Driven Development and much more! Show Notes online - https://thinkingelixir.com/podcast-episodes/023-gleam-and-static-types-with-louis-pilfold

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.

Your favorite features of Type Systems in one episode! Interfaces, Generics, ADT, Type Classes and Dependent Types. We'll talk about what they are and how they shape the way we work. Code Podcast Forum: https://discuss.codepodcast.com/t/episode-5-type-systems/22 Episode produced by: Andrey Salomatin https://twitter.com/flpvsk Michael Beschastnov michael@codepodcast.com Guests (in order of appearance): Joseph Abrahamson https://twitter.com/sdbo Radoslav Kirov https://twitter.com/radokirov Erlend Hamberg https://twitter.com/ehamberg Edwin Brady https://twitter.com/edwinbrady Special thanks to our reviewers, this time: Adriano Melo https://twitter.com/AdrianoMelo Roman Liutikov https://twitter.com/roman01la If you'd like to help us make the podcast better *and* get episodes earlier, consider becoming a reviewer: https://gist.github.com/filipovskii/f12685bc74a425ba651c736fb5e3e5ae ## Links: Basics Benjamin C. Pierce "Types and Programming Languages" https://www.cis.upenn.edu/~bcpierce/tapl/ A draft of the book available for free: http://ropas.snu.ac.kr/~kwang/520/pierce_book.pdf Rob Nederpelt and Herman Geuvers "Type Theory and formal proof" http://www.win.tue.nl/~wsinrpn/book_type_theory.htm Robert Harper "Practical Foundations for Programming Languages" https://www.cs.cmu.edu/~rwh/pfpl.html Interview with Jesper Louis Andersen about Erlang, Haskell, OCaml, Go, Idris, the JVM, software and protocol design — PART I https://notamonadtutorial.com/interview-with-jesper-louis-andersen-about-erlang-haskell-ocaml-go-idris-the-jvm-software-and-b0de06440fbd#.rawqi9bvp Paper by Xavier Leroy "Manifest Types, Modules, and Separate Compilation" (1994) http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.3950 Paper by Conor McBride and Ross Paterson "FUNCTIONAL PEARL: Applicative programming with effects" http://strictlypositive.org/IdiomLite.pdf ## Links: Idris Edwin Brady "Type-Driven Development with Idris" http://tinyurl.com/typedd ## Links: TypeScript http://www.typescriptlang.org/ ## Links: Haskell Christopher Allen and Julie Moronuki "Haskell Programming from First Principles" http://haskellbook.com/ Learn you some Haskell http://learnyouahaskell.com/ ## Links: Scala Paul Chiusano and Rúnar Bjarnason "Functional Programming in Scala" https://www.manning.com/books/functional-programming-in-scala ##Links: OCaml Yaron Minsky, Anil Madhavapeddy, Jason Hickey "Real World Ocaml" https://realworldocaml.org A chapter from "Real World Ocaml" about Objects https://realworldocaml.org/v1/en/html/objects.html OCaml Documentation http://caml.inria.fr/pub/docs/manual-ocaml/ Effective ML (video) https://blogs.janestreet.com/effective-ml-video/ ## Links: Discussions What exactly makes the Haskell type system so revered (vs say, Java)? http://softwareengineering.stackexchange.com/questions/279316/what-exactly-makes-the-haskell-type-system-so-revered-vs-say-java What is a Functor? http://stackoverflow.com/questions/2030863/in-functional-programming-what-is-a-functor#2031421 ADTs vs Inheritance http://stackoverflow.com/questions/3271974/why-adts-are-good-and-inheritance-is-bad Existential vs Universal Typess http://stackoverflow.com/questions/14299638/existential-vs-universally-quantified-types-in-haskell#14299983 Subclassing vs Subtyping http://www.cs.princeton.edu/courses/archive/fall98/cs441/mainus/node12.html Why Haskell has no subtyping https://www.reddit.com/r/haskell/comments/423o0c/why_no_subtypingsubtype_polymorphism/ Haskell vs Java type systems http://softwareengineering.stackexchange.com/questions/279316/what-exactly-makes-the-haskell-type-system-so-revered-vs-say-java ## Music Mid-Air! @mid_air