Podcast appearances and mentions of Benjamin C Pierce

02:35 - Philip’s Superpower: Being Not Afraid of Mathematics 04:07 - Programming Language Foundations in Agda (https://plfa.github.io/) Propositions as Types (https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf) Isomorphism (https://en.wikipedia.org/wiki/Isomorphism) Software Foundations by Benjamin C. Pierce (https://www.goodreads.com/book/show/13413455-software-foundations) The Coq Proof Assistant (https://coq.inria.fr/) 15:32 - Using a Proof Assistant 22:57 - Human Creativity + Insight QuickCheck (http://hackage.haskell.org/package/QuickCheck) CompCert (http://compcert.inria.fr/) 30:02 - Specifications Use of Formal Methods at Amazon Web Services (https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf) The Evolution of Testing Methodology at AWS: From Status Quo to Formal Methods with TLA+ (https://www.infoq.com/presentations/aws-testing-tla/) How Amazon web services uses formal methods (https://dl.acm.org/citation.cfm?id=2699417) 35:25 - How To Translate Abstract Concepts So Practitioners Can Use Them Reflections: Rein: The way we are taught math makes us hate it. Jess: There’s a difference between learning the foundations of programming and learning the skills of programming Chanté: How do we make conversations like this more accessible? Jacob: Ways of getting quick and seamless feedback as you are writing a program. Joint Cognitive Systems: Foundations of Cognitive Systems Engineering (https://www.amazon.com/Joint-Cognitive-Systems-Foundations-Engineering/dp/0849328217) This episode was brought to you by @therubyrep (https://twitter.com/therubyrep) of DevReps, LLC (http://www.devreps.com/). To pledge your support and to join our awesome Slack community, visit patreon.com/greaterthancode (https://www.patreon.com/greaterthancode) To make a one-time donation so that we can continue to bring you more content and transcripts like this, please do so at paypal.me/devreps (https://www.paypal.me/devreps). You will also get an invitation to our Slack community this way as well. Amazon links may be affiliate links, which means you’re supporting the show when you purchase our recommendations. Thanks! Special Guest: Philip Wadler.

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

02:37 - Dave Thomas Introduction Twitter Blog The Pragmatic Bookshelf 04:17 - How Dave Got Started in Programming 06:34 - Tools and Constraints “An Enthusiast’s Problem”? Is the focus on tools a form of cargo culting? Leadism Over Chosen Technologies and Its’ Effect on Innovation Switching Tools and Making Excuses 19:29 - Limerence Love and Limerence: The Experience of Being in Love by Dorothy Tennov Irrational Interest and Defensiveness 28:54 - Ruby = Happiness: Does it Hurt? 31:00 - Tools and Falling in Love with Tools Fear of Falling Behind; Fear of Irrelevancy Different Tools for Different Contexts 35:08 - When Do You Learn? When Do You Train? (Not Falling Behind) 38:01 - Choosing Similar Tools and Technologies vs Choosing Different Tools and Technologies Gulp => Grunt => Browserify Example Pragmatic Thinking and Learning: Refactor Your Wetware by Andy Hunt 43:36 - Relationships and Identities 46:08 - Looking Forward vs Looking Back (Knowing Your History) Resources, Curriculum: Structure and Interpretation of Computer Programs - 2nd Edition (MIT Electrical Engineering and Computer Science) by Harold Abelson (SICP) Smalltalk Best Practice Patterns by Kent Beck Types and Programming Languages by Benjamin C. Pierce    The Art of Computer Programming by Donald Knuth (Series) Communicating Sequential Processes (CSP) Brainstorming Example 01:01:48 - Is the rampant use of social media hindering the learning of big ideas? Self-Curation = Key 01:08:15 - How You Learn a Language / Decide You Like a Language Sudoku Solver Markdown Parser Picks Slack (Dave) Why Does E=mc2? (And Why Should We Care?) by Brian Cox and Jeff Forshaw (Dave) Philly Emerging Tech Conference  (Dave)  

02:37 - Dave Thomas Introduction Twitter Blog The Pragmatic Bookshelf 04:17 - How Dave Got Started in Programming 06:34 - Tools and Constraints “An Enthusiast’s Problem”? Is the focus on tools a form of cargo culting? Leadism Over Chosen Technologies and Its’ Effect on Innovation Switching Tools and Making Excuses 19:29 - Limerence Love and Limerence: The Experience of Being in Love by Dorothy Tennov Irrational Interest and Defensiveness 28:54 - Ruby = Happiness: Does it Hurt? 31:00 - Tools and Falling in Love with Tools Fear of Falling Behind; Fear of Irrelevancy Different Tools for Different Contexts 35:08 - When Do You Learn? When Do You Train? (Not Falling Behind) 38:01 - Choosing Similar Tools and Technologies vs Choosing Different Tools and Technologies Gulp => Grunt => Browserify Example Pragmatic Thinking and Learning: Refactor Your Wetware by Andy Hunt 43:36 - Relationships and Identities 46:08 - Looking Forward vs Looking Back (Knowing Your History) Resources, Curriculum: Structure and Interpretation of Computer Programs - 2nd Edition (MIT Electrical Engineering and Computer Science) by Harold Abelson (SICP) Smalltalk Best Practice Patterns by Kent Beck Types and Programming Languages by Benjamin C. Pierce    The Art of Computer Programming by Donald Knuth (Series) Communicating Sequential Processes (CSP) Brainstorming Example 01:01:48 - Is the rampant use of social media hindering the learning of big ideas? Self-Curation = Key 01:08:15 - How You Learn a Language / Decide You Like a Language Sudoku Solver Markdown Parser Picks Slack (Dave) Why Does E=mc2? (And Why Should We Care?) by Brian Cox and Jeff Forshaw (Dave) Philly Emerging Tech Conference  (Dave)  

02:37 - Dave Thomas Introduction Twitter Blog The Pragmatic Bookshelf 04:17 - How Dave Got Started in Programming 06:34 - Tools and Constraints “An Enthusiast’s Problem”? Is the focus on tools a form of cargo culting? Leadism Over Chosen Technologies and Its’ Effect on Innovation Switching Tools and Making Excuses 19:29 - Limerence Love and Limerence: The Experience of Being in Love by Dorothy Tennov Irrational Interest and Defensiveness 28:54 - Ruby = Happiness: Does it Hurt? 31:00 - Tools and Falling in Love with Tools Fear of Falling Behind; Fear of Irrelevancy Different Tools for Different Contexts 35:08 - When Do You Learn? When Do You Train? (Not Falling Behind) 38:01 - Choosing Similar Tools and Technologies vs Choosing Different Tools and Technologies Gulp => Grunt => Browserify Example Pragmatic Thinking and Learning: Refactor Your Wetware by Andy Hunt 43:36 - Relationships and Identities 46:08 - Looking Forward vs Looking Back (Knowing Your History) Resources, Curriculum: Structure and Interpretation of Computer Programs - 2nd Edition (MIT Electrical Engineering and Computer Science) by Harold Abelson (SICP) Smalltalk Best Practice Patterns by Kent Beck Types and Programming Languages by Benjamin C. Pierce    The Art of Computer Programming by Donald Knuth (Series) Communicating Sequential Processes (CSP) Brainstorming Example 01:01:48 - Is the rampant use of social media hindering the learning of big ideas? Self-Curation = Key 01:08:15 - How You Learn a Language / Decide You Like a Language Sudoku Solver Markdown Parser Picks Slack (Dave) Why Does E=mc2? (And Why Should We Care?) by Brian Cox and Jeff Forshaw (Dave) Philly Emerging Tech Conference  (Dave)