Podcast appearances and mentions of philip wadler

The subject of this episode's paper — Propositions as Types by Philip Wadler — is one of those grand ideas that makes you want to go stargazing. To stare out into space and just disassociate from your body and become one with the heavens. Everything — life, space, time, existence — all of it is a joke! A cosmic ribbing delivered by the laws of the universe or some higher power or, perhaps, higher order. Humanity waited two thousand years, from the time of the ancient Greeks through until the 1930s, for a means to answer questions of calculability, when three suddenly arrived all at once: General recursive functions by Gödel in 1934, with functions of sets of natural numbers. Lambda calculus by Alonzo Church in 1936, with anonymous single-variable functions. Turing machines by Alan Turing in 1937, with a process for evaluating symbols on a tape. Then it was discovered that these three models of computation were, in fact, perfectly equivalent. That any statement made in one could be made in the others. A striking coincidence, sure, but not without precedent. But then it was quietly determined (in 1934, again in 1969, and finally published in 1980) that computation itself is in a direct correspondence with logic. That every proposition in a given logic corresponds with a type in a given programming language, every proof corresponds with a program, and the simplification of the proof corresponds with the evaluation of the program. The implications boggle the mind. How could this be so? Well, how could it be any other way? Why did it take so long to discover? What other discoveries like this are perched on the precipice of revelation? Philip Wadler is here to walk us through this bit of history, suggest answers to some of these questions, and point us in a direction to search for more. And we are here, dear listener, to level with you that a lot of this stuff is miserably hard to approach, presented with the symbols and language of formal logic that is so often inscrutable to outsiders. By walking you through Wadler's paper (and the much more approachable Strange Loop talk), and tying it in with the cultural context of modern functional programming, we hope you'll gain an appreciation for this remarkable, divine pun that sits beneath all of computation. Links => patreon.com/futureofcoding — but only if you back the Visual Programming tier!! I'm warning you! Wadler's Strange Loop talk Propositions as Types Cocoon is good. It's not, like, Inside or Limbo good, but it's good. Actually, just play Inside. Do that ASAP. Hollow Knight, also extremely good. Can't wait for Silksong. But seriously, if you're reading this and have haven't played Inside, just skip this episode of the podcast and go play Inside. It's like 3 hours long and it's, like, transformatively great. Chris Martens has done some cool work (eg) bringing together linear logic and games. Meh: Gödel, Escher, Bach by Douglas Hofstadter Yeh: Infinity and the Mind by Rudy Rucker Heh: To Mock a MockingBird by Raymond Smullyan. The hierarchy of automata Games: Agency as Art The Incredible Proof Machine is what some would call a "visual programming language" because proofs are programs. But it's actually really cool and fun to play with. Approach it like a puzzle game, and give it 10 minutes or so to get its hooks into you. "Stop Doing Logic" is part of the Stop Doing Math meme. Unrelated: Ivan's song Don't Do Math. Bidirectional Type Checking, a talk by David Christiansen List Out of Lambda, a blog post by Steve Losh Nobody noticed that these links were silly last time, so this time I'm drawing more attention to it: Ivan: Mastodon • Email Jimmy: Mastodon • Twitter This link is legit: DM us in the FoC Slack https://futureofcoding.org/episodes/068See omnystudio.com/listener for privacy information.

Today we're discussing the so-called "incommensurability" paper: The Structure of a Programming Language Revolution by Richard P. Gabriel. In the pre-show, Jimmy demands that Ivan come right out and explain himself, and so he does, to a certain extent at least. In the post-show, Jimmy draws such a thick line between programming and philosophy that it wouldn't even look out of place on Groucho Marx's face. Next episode, we will be covering the Worse is Better family of thought products, so take 15 minutes to read these three absolute bangers if you'd like to be ahead of the game: The Rise of Worse is Better by Richard P. Gabriel Worse is Better is Worse, definitely not by Richard P. Gabriel Is Worse Really Better? by Richard P. Gabriel Links Phlogiston Theory Phlogiston the excellent chiptune musician. Bright Eyes - First Day of My Life, by Conor Oberst. Not to be confused with Conal Elliott, who introduced the original meaning of functional reactive programming in his work on Fran. Peter Gabriel - Games Without Frontiers Pilot: A Step Toward Man-Computer Symbiosis Jimmy's talk Paradigms Without Progress: Kuhnian Reflections on Programming Practice There's some sporadic discussion of Philip Wadler (who Ivan playfully calls "Phil"), specifically his claim that programming languages have some bits that are invented and some bits that are discovered. While we're here, make sure you've seen the best 15 seconds in Strange Loop history. Peter Naur's Programming as Theory Building Sponsors CarrotGrid — They don't have a web presence (weird, hey?) but they're working on an interesting problem at the intersection of data, so listen to the short ad in the episode to find out more. St. Jude Children's Research Hospital — Instead of running our usual sponsors today, we'd like to direct your attention to this humanitarian cause. September is Childhood Cancer Awareness Month, and our friends (can we call them that?) at Relay.fm are running a pledge drive. If you have any spare coins in your couch cushions, or a few million left over from your last exit, you'd be hard pressed to find a more deserving way to invest them. Donate here. Show notes for this episode can be found at futureofcoding.org/episodes/58See omnystudio.com/listener for privacy information.

I give a brief glimpse at Phil Wadler's important paper "The Girard-Reynolds Isomorphism", which is quite relevant for Relational Type Theory as it shows that relational semantics for the usual type for Church-encoded natural numbers implies induction. RelTT uses a generalization of these ideas to derive induction for any positive type family.

I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent. This is similar to proofs one can find in a paper of Philip Wadler's titled "The Girard-Reynolds Isomorphism", which I plan to discuss in the next episode.

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.

Philip Wadler is a Professor of Theoretical Computer Science at the University of Edinburgh and a Senior Research Fellow for IOHK. In this episode he discusses the Plutus programming language used for smart contracts on the Cardano Platform. Watch Episode 10 and view more information on Youtube: https://youtu.be/8P_cZ5V0-4I

Evolving software under constrained resources is a challenge, and I think we kid ourselves when we don't admit this. Software that is providing value often grows in scope until it is a mess.  Today I talk to Wade Waldron about how avoid this situation or recover from it. Big ball of mud is the title of a paper presented at the 1997 Patterns Languages of Programs conference and I think it is super interesting. The researchers went out into the field to see what architectures software in industry were following. Big Ball of mud is what they found, along with other 6 other patterns with names like "sweep it under the rug" and reconstruction, which is the throw it away and start again pattern. Links: Big Ball Of Mud Paper Hexagonal Architecture Reactive Foundations Course Reactive Advanced Course Check out other episodes like this Philip Wadler: https://corecursive.com/021-gods-programming-language-with-philip-wadler/ This podcast originally published here : https://corecursive.com/22-big-ball-of-mud-architecture-and-services-with-wade-waldron/

Today I talk to Professor Philip Wadler, a very accomplished programming language researcher.  Phil walks us through a principle that has guided his career.  That principle is that typed lambda calculus is not invented but a discovery of a deep truth. It is something connected to the mathematical underpinning of the universe itself. It follows from this that functional programming languages are therefore more correct or more deeply justified and fundamental than other languages.  I am probably stating things in a stronger fashion than Phil is comfortable with, but I like fp, so I can be a little hyperbolic. While explaining this principle, that has guided his career, Phil takes us through the history of computer science.  We start with Turing and Alonzo Church.  Eventually we get to what the movie Independence Day got wrong and what language a theoretical creator deity would program in. Show notes: talk paper   Web page for this episode CoRecursive On Twitter CoRecursive On Itunes

AiA 147: Codelyzer and Static Analysis Tools for Angular with Minko Gechev The week on Adventures in Angular features panelists Alyssa Nicoll, Shi Resnick, Lukas Ruebbelk, and Charles Max Wood. The special guest this week is Minko Gechev who is here to discuss Codelyzer. Minko is currently working on a start up. Angular JavaScript is the programming language that excites him the most. How do you work in a start up and still have free time? He tries to find an overlap between the work he's doing in the startup and work he does in his spare time. This is why he had previous work that was completely Angular (Angular Seed). This startup is more complicated because the overlap isn't as much. What is Codelyzer?       Last year, he worked on the Angular Style Guide. He thought it was a good idea to have an automated way to verify a given project that follows the Angular Style Guide. He built on top of that and built Angular and provided similar style checks on top of templates, Angular CSS Styles inside of the components, and the Angular expressions inside of the templates. Codelyzer is a tool for static code analysis for Angular applications. How is it used?                                               It can be used as a set of rules on top of tslint. You install it with mpm. Then tslint performs static analysis and verifies whether the source code follows some style guidelines that our team has agreed upon. When Codelyzer is used, we can also analyze the templates on Angular applications. After that, you can confirm it follows these rules by running tslint on top of the entire project. How many of the default tslint rules do you agree with? Minko states that that is a lot of tslint and Angular rules that align and that he agrees with most of them. He does admit there are some he finds annoying, such as specific semi colon rules. Overall, he believes that if the team has agreed upon the rule, it is following in order to avoid arguing. What do you recommend as the best way to add Codelyzer to a project that started without it? He thinks you should add one rule at a time. All the wordings will be fixed one by one, eventually fixing the entire project. He has also started working on style analysis on top of the application, which is performance analysis. He doesn’t know what data the application will process. But he still considers that a given component will have performance if it has a huge -- in the template. So static analysis we can find such templates and eventually warn the users about eventual performance issues that are possible. How hard is it to add or change in Codelyzer? It might be slightly harder compared to tslint because there are more things that can be statically verified. In Tslint there's a visitor pattern. There is a classical design from the Ganga; it is used for the reversal of syntax 3 of a Typescript code. So when you implement the visitor pattern, you visit a specific construct, verify whether the name follows some guidelines. It is pretty much the same thing in Codelyzer but you can also implement the same visitor pattern for visiting the template of the component. Currently, the project has more than 20 contributors. It looks complicated but not if you spend 30 to 40 minutes looking at the code. What was the motivation behind going deep into Angular? The style was easy for static (automated) verification. This way saved a lot of time from code reviews. Code reviews still have to be performed, but at least can skip the verification from style guides because they can be automatically done. He likes compilers, it is the front end of a compiler: analyzing Syntax 3 part of a compiler itself interesting algorithms. There is another rule from Codelyzer being worked on that isn't completely stable yet. It is to find out which styles are actually used inside of the template. Codelyzer can find out some of the styles that are no longer applied to some of the styles within the template. This is not ready yet but it will be ready in a couple of configurations. Is the idea of searching through of finding either redundant or non-used style, is this something Codelyzer's doing for the very first time (no one has ever done it) or are there tools that this would replace? For Angular, there is no other tool like that. JavaScript or HTML may be close. The Browser can do that. If I want to write a rule do I take the abstract syntax and tell it what to look for? How does that work? You can’t learn it by heart, so I usually copy and paste the existing code and then modify it. It is a standard typescript rule so you need to provide an abstract rule; you'll need to provide the visitor. If the rule is super complicated, you need four visitors. Are you relying on tslint to break things down into tokens and the abstract syntax and then doing the work from there? Yeah. I did some extensions of tslint. Just extending tslint because it would have been too much work to create something from scratch. He is relying on tslint’s error reporting. So in order to set this up on a CI machine, it needs to be able to run node and install some mpm packages? Yes. Run node, install tslint, install Codelyzer and have this rule directory with the Codelyzer rules inside tslint. Is there a visual proof for knowing what the rule does? There is documentation on codelyzer.com/rules. Picks: Shi: Reflect API Driving on the right side of the road Minko Gechev Alyssa: Apple Airpods:https://www.apple.com/airpods Crutches Lukas: iPhone 7+ portrait mode: https://techcrunch.com/2016/09/21/hands-on-with-the-iphone-7-plus-crazy-new-portrait-mode/ Vulfpeck-1612: https://www.youtube.com/watch?v=jRHQPG1xd9o Charles: Angular Dev Summit www.angulardevsummit.com Minko: Pixel: https://madeby.google.com/phone/ Angular IO: https://angular.io/ Philip Wadler’s Monads for Functional Programming: http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf  

AiA 147: Codelyzer and Static Analysis Tools for Angular with Minko Gechev The week on Adventures in Angular features panelists Alyssa Nicoll, Shi Resnick, Lukas Ruebbelk, and Charles Max Wood. The special guest this week is Minko Gechev who is here to discuss Codelyzer. Minko is currently working on a start up. Angular JavaScript is the programming language that excites him the most. How do you work in a start up and still have free time? He tries to find an overlap between the work he's doing in the startup and work he does in his spare time. This is why he had previous work that was completely Angular (Angular Seed). This startup is more complicated because the overlap isn't as much. What is Codelyzer?       Last year, he worked on the Angular Style Guide. He thought it was a good idea to have an automated way to verify a given project that follows the Angular Style Guide. He built on top of that and built Angular and provided similar style checks on top of templates, Angular CSS Styles inside of the components, and the Angular expressions inside of the templates. Codelyzer is a tool for static code analysis for Angular applications. How is it used?                                               It can be used as a set of rules on top of tslint. You install it with mpm. Then tslint performs static analysis and verifies whether the source code follows some style guidelines that our team has agreed upon. When Codelyzer is used, we can also analyze the templates on Angular applications. After that, you can confirm it follows these rules by running tslint on top of the entire project. How many of the default tslint rules do you agree with? Minko states that that is a lot of tslint and Angular rules that align and that he agrees with most of them. He does admit there are some he finds annoying, such as specific semi colon rules. Overall, he believes that if the team has agreed upon the rule, it is following in order to avoid arguing. What do you recommend as the best way to add Codelyzer to a project that started without it? He thinks you should add one rule at a time. All the wordings will be fixed one by one, eventually fixing the entire project. He has also started working on style analysis on top of the application, which is performance analysis. He doesn’t know what data the application will process. But he still considers that a given component will have performance if it has a huge -- in the template. So static analysis we can find such templates and eventually warn the users about eventual performance issues that are possible. How hard is it to add or change in Codelyzer? It might be slightly harder compared to tslint because there are more things that can be statically verified. In Tslint there's a visitor pattern. There is a classical design from the Ganga; it is used for the reversal of syntax 3 of a Typescript code. So when you implement the visitor pattern, you visit a specific construct, verify whether the name follows some guidelines. It is pretty much the same thing in Codelyzer but you can also implement the same visitor pattern for visiting the template of the component. Currently, the project has more than 20 contributors. It looks complicated but not if you spend 30 to 40 minutes looking at the code. What was the motivation behind going deep into Angular? The style was easy for static (automated) verification. This way saved a lot of time from code reviews. Code reviews still have to be performed, but at least can skip the verification from style guides because they can be automatically done. He likes compilers, it is the front end of a compiler: analyzing Syntax 3 part of a compiler itself interesting algorithms. There is another rule from Codelyzer being worked on that isn't completely stable yet. It is to find out which styles are actually used inside of the template. Codelyzer can find out some of the styles that are no longer applied to some of the styles within the template. This is not ready yet but it will be ready in a couple of configurations. Is the idea of searching through of finding either redundant or non-used style, is this something Codelyzer's doing for the very first time (no one has ever done it) or are there tools that this would replace? For Angular, there is no other tool like that. JavaScript or HTML may be close. The Browser can do that. If I want to write a rule do I take the abstract syntax and tell it what to look for? How does that work? You can’t learn it by heart, so I usually copy and paste the existing code and then modify it. It is a standard typescript rule so you need to provide an abstract rule; you'll need to provide the visitor. If the rule is super complicated, you need four visitors. Are you relying on tslint to break things down into tokens and the abstract syntax and then doing the work from there? Yeah. I did some extensions of tslint. Just extending tslint because it would have been too much work to create something from scratch. He is relying on tslint’s error reporting. So in order to set this up on a CI machine, it needs to be able to run node and install some mpm packages? Yes. Run node, install tslint, install Codelyzer and have this rule directory with the Codelyzer rules inside tslint. Is there a visual proof for knowing what the rule does? There is documentation on codelyzer.com/rules. Picks: Shi: Reflect API Driving on the right side of the road Minko Gechev Alyssa: Apple Airpods:https://www.apple.com/airpods Crutches Lukas: iPhone 7+ portrait mode: https://techcrunch.com/2016/09/21/hands-on-with-the-iphone-7-plus-crazy-new-portrait-mode/ Vulfpeck-1612: https://www.youtube.com/watch?v=jRHQPG1xd9o Charles: Angular Dev Summit www.angulardevsummit.com Minko: Pixel: https://madeby.google.com/phone/ Angular IO: https://angular.io/ Philip Wadler’s Monads for Functional Programming: http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf  

AiA 147: Codelyzer and Static Analysis Tools for Angular with Minko Gechev The week on Adventures in Angular features panelists Alyssa Nicoll, Shi Resnick, Lukas Ruebbelk, and Charles Max Wood. The special guest this week is Minko Gechev who is here to discuss Codelyzer. Minko is currently working on a start up. Angular JavaScript is the programming language that excites him the most. How do you work in a start up and still have free time? He tries to find an overlap between the work he's doing in the startup and work he does in his spare time. This is why he had previous work that was completely Angular (Angular Seed). This startup is more complicated because the overlap isn't as much. What is Codelyzer?       Last year, he worked on the Angular Style Guide. He thought it was a good idea to have an automated way to verify a given project that follows the Angular Style Guide. He built on top of that and built Angular and provided similar style checks on top of templates, Angular CSS Styles inside of the components, and the Angular expressions inside of the templates. Codelyzer is a tool for static code analysis for Angular applications. How is it used?                                               It can be used as a set of rules on top of tslint. You install it with mpm. Then tslint performs static analysis and verifies whether the source code follows some style guidelines that our team has agreed upon. When Codelyzer is used, we can also analyze the templates on Angular applications. After that, you can confirm it follows these rules by running tslint on top of the entire project. How many of the default tslint rules do you agree with? Minko states that that is a lot of tslint and Angular rules that align and that he agrees with most of them. He does admit there are some he finds annoying, such as specific semi colon rules. Overall, he believes that if the team has agreed upon the rule, it is following in order to avoid arguing. What do you recommend as the best way to add Codelyzer to a project that started without it? He thinks you should add one rule at a time. All the wordings will be fixed one by one, eventually fixing the entire project. He has also started working on style analysis on top of the application, which is performance analysis. He doesn’t know what data the application will process. But he still considers that a given component will have performance if it has a huge -- in the template. So static analysis we can find such templates and eventually warn the users about eventual performance issues that are possible. How hard is it to add or change in Codelyzer? It might be slightly harder compared to tslint because there are more things that can be statically verified. In Tslint there's a visitor pattern. There is a classical design from the Ganga; it is used for the reversal of syntax 3 of a Typescript code. So when you implement the visitor pattern, you visit a specific construct, verify whether the name follows some guidelines. It is pretty much the same thing in Codelyzer but you can also implement the same visitor pattern for visiting the template of the component. Currently, the project has more than 20 contributors. It looks complicated but not if you spend 30 to 40 minutes looking at the code. What was the motivation behind going deep into Angular? The style was easy for static (automated) verification. This way saved a lot of time from code reviews. Code reviews still have to be performed, but at least can skip the verification from style guides because they can be automatically done. He likes compilers, it is the front end of a compiler: analyzing Syntax 3 part of a compiler itself interesting algorithms. There is another rule from Codelyzer being worked on that isn't completely stable yet. It is to find out which styles are actually used inside of the template. Codelyzer can find out some of the styles that are no longer applied to some of the styles within the template. This is not ready yet but it will be ready in a couple of configurations. Is the idea of searching through of finding either redundant or non-used style, is this something Codelyzer's doing for the very first time (no one has ever done it) or are there tools that this would replace? For Angular, there is no other tool like that. JavaScript or HTML may be close. The Browser can do that. If I want to write a rule do I take the abstract syntax and tell it what to look for? How does that work? You can’t learn it by heart, so I usually copy and paste the existing code and then modify it. It is a standard typescript rule so you need to provide an abstract rule; you'll need to provide the visitor. If the rule is super complicated, you need four visitors. Are you relying on tslint to break things down into tokens and the abstract syntax and then doing the work from there? Yeah. I did some extensions of tslint. Just extending tslint because it would have been too much work to create something from scratch. He is relying on tslint’s error reporting. So in order to set this up on a CI machine, it needs to be able to run node and install some mpm packages? Yes. Run node, install tslint, install Codelyzer and have this rule directory with the Codelyzer rules inside tslint. Is there a visual proof for knowing what the rule does? There is documentation on codelyzer.com/rules. Picks: Shi: Reflect API Driving on the right side of the road Minko Gechev Alyssa: Apple Airpods:https://www.apple.com/airpods Crutches Lukas: iPhone 7+ portrait mode: https://techcrunch.com/2016/09/21/hands-on-with-the-iphone-7-plus-crazy-new-portrait-mode/ Vulfpeck-1612: https://www.youtube.com/watch?v=jRHQPG1xd9o Charles: Angular Dev Summit www.angulardevsummit.com Minko: Pixel: https://madeby.google.com/phone/ Angular IO: https://angular.io/ Philip Wadler’s Monads for Functional Programming: http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf  

In this episode I talk with Professor Philip Wadler. We talk the correspondence between mathematics and computation, his research into concurrent distributed systems, and other research in the area with ABCD and BETTY.