Functional Geekery

In this episode I talk with Nikhil Swamy. We talk F*, dependent types, proving software, Dijkstra Monads, Project Everest for verified HTTPS, and more. Our Guest, Nikhil Swamy Nikhil Swamy F* Announcements CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit http://www.scalawave.io/ to find out more and sign up for their newsletter for updates. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. The 2016 Clojure Conj will be taking place in Austin, TX on December 1st – 3rd. Visit http://2016.clojure-conj.org for more information and to register. Lambda Days will be taking place again on the 9th and 10th of February 2017. Visit www.lambdadays.org to submit your talk and keep updated as more information becomes available. ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit www.clojured.de to submit your talk, get tickets and keep updated as more information becomes available. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Nik Microsoft Research Labs F* How Nik got into proving software Coq Agda Cyclone F* as a combination of interactive and automated proofs SMT Solvers Dependent Types and Dependent Type systems as provers Embracing Effects in F* Using Type Systems to prove things about your program Idris Expressing a list as sorted using Dependent Types Types as Sets Testing is a means try to disprove your program Dependent Types as a means to verify your program Lean Typed Lambda Calculus Proving that a list is sorted Quicksort Hints and Lemmas Curry-Howard Isomorphism F* Tutorial F* Quicksort Tutorial Example POPL 2017 Dijkstra Monads for Free Weakest Pre-condition of a program Weakest Pre-condition adapted to monads Improvement of tooling for proving software in the past 10 years Project Everest Inria Build and deploy verified drop in replacement for HTTPS stack HTTPS TLS – Transport Layer Security OpenSSL Heartbleed X.509 Spartan Writing programs at the Assembly level and proving them correct Dafny Z3 Theorem Prover F* being used to prove Project Everest’s correctness Euro Security and Privacy F* on Github F* Slack channel F* mailing list “Specify before proving” “Try to specify before even writing a line of code” F* for the Masses blog As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Simon Thompson. We cover a broad range of topics from a history of functional programming from the 1980s, to his involvement with Haskell, teaching Haskell and Erlang, the functional programming hype cycle, recent and future work, and much, much more. Our Guest, Simon Thompson https://www.cs.kent.ac.uk/people/staff/sjt/ @thompson_si on Twitter https://profsjt.blogspot.co.uk/ Announcements EuroClojure is coming up in Bratislava, Slovakia from October 25-26. Visit http://euroclojure.org/ to find out more, register, or sign up for their mailing list. The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit http://scala.io/ for more information and to register. CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit http://www.scalawave.io/ to find out more and sign up for their newsletter for updates. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. The 2016 Clojure Conj will be taking place in Austin, TX on December 1st – 3rd. Visit http://2016.clojure-conj.org for more information and to register. Lambda Days will be taking place again on the 9th and 10th of February 2017. Visit www.lambdadays.org to submit your talk and keep updated as more information becomes available. ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit www.clojured.de to submit your talk, get tickets and keep updated as more information becomes available. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Professor Thompson University of Kent Overview of Functional Programming in the 1980’s Functional Programming and its Applications: An Advanced Course by Peter Henderson, David Turner, and John Darlington SASL – Saint Andrew’s Static Language Alice Hope KRC – Kent Recursive Calculator Miranda Functional Programming and Computer Architecture conference “Revolutionary new architectures that only functional programming languages would work with” David Turner saying “I am sure by 2000, mathematicians will use automated proof as a matter of course” Haskell Simon Peyton Jones What Professor Thompson worked on in Haskell Haskell: The Craft of Functional Programming Type Theory and Functional Programming [pdf] Work on input in Miranda as streams of Input and Output Year of Programming Input/Output as combinators which became the precursor to monads Interactive functional programs: a method and a formal semantics Turning Haskell programs into logical formulas Ericsson and Erlang Open Source strengthening Haskell and Erlang Cabal Hackage WhatsApp Elixir Scala Java View of the recent hype cycle of functional programming “People are so scared to program Java on a 100-core machine, they haven’t come into the mainstream” Seeing the change in jobs doing functional programming Professor Thompson’s work over the past 10 years Refactoring tooling Randomly generate programs and randomly apply refactorings OCaml Z3 SMT solver CakeML Prove refactoring in CakeML JaneStreet Wrangler Creating a DSL for scripting refactorings Overview of differences between Haskell and Erlang Laziness in Haskell Differences between the size of the languages Simulating a dependency typed language in Haskell Differences in the rates of release in new versions of the languages Central place to have a place to upload and download software libraries Differences between first exposures to Erlang and Haskell for students Erlang is more approachable due to smaller syntax Notation for lists in Erlang is a stumbling block for students Erlang’s weak types as a weakness for beginners Dialyzer Success Typing Complexity of Type System in Haskell and errors for beginners Benefit of simple syntax and concurrency story for beginners in Erlang Haskell as a laboratory for concurrency ideas Thoughts on teaching students functional programming ideas Erlang MOOC preliminary launch Erlang MOOC to be coming in Spring 2017 Recursion Threads vs Processes in Erlang for experienced programmers “Let the concurrency in the program mirror the concurrency in the real world” “It would be lovely to do some work […] to validate these claims” OSCON CodeMesh Importance of bottom up development of learning materials Peter Landin Semantic Seminar Erlang MOOC composed of two “mini-MOOCs” “Give it a try” “Different languages have different things to offer” As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Bartosz Milewski. We talk his introduction to category theory, teaching category theory, comparison of Monads and other composition patterns in functional programming to composition patterns in object oriented programming, and finish with some philosophical thoughts on category theory. Our Guest, Bartosz Milewski @bartoszmilewski on Twitter https://bartoszmilewski.com/ Bartosz’s YouTube channel for his category theory videos Announcements EuroClojure is coming up in Bratislava, Slovakia from October 25-26. Visit http://euroclojure.org/ to find out more, register, or sign up for their mailing list. The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit http://scala.io/ for more information and to register. CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit http://www.scalawave.io/ to find out more and sign up for their newsletter for updates. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. The 2016 Clojure Conj will be taking place in Austin, TX on December 1st – 3rd. Visit http://2016.clojure-conj.org for more information and to register. Lambda Days will be taking place again on the 9th and 10th of February 2017. Visit www.lambdadays.org to submit your talk and keep updated as more information becomes available. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Bartosz Bartosz’s videos on category theory on YouTube How Bartosz became exposed to category theory Elegant code, and what does it mean for code to be elegant? Exposure to functional programming through C++ Template meta-programming in C++ Andrei Alexandrescu’s Modern C++ Design: Generic Programming and Design Patterns Applied Haskell Translating functional solutions in Haskell to C++ Exposure to category theory Categories for the Working Mathematician Edward Kmett Understanding category theory through examples What clicked about category theory once Bartosz “got it” “Category Theory can be simplified to just two things, composition and identity” Futures in C++ Futures are monads “Monads are just about how to compose stuff” Bartosz’s posts on Futures – Broken promises–C++0x futures – Futures done right – C++17: I See a Monad in Your Future! “You cannot design a good library, if you don’t understand category theory, or at least elements of it” Category of Types and Functions “A composition is the essence of a category” “A monad is a way about composing side-effects” Category theory patterns become hard to understand because they are so general Function composition in an imperative language “A monad is the overloading of a semicolon” Background of attendees in his courses Interest in teaching category theory to artists and other domains Curry-Howard Isomorphism “You take a concept from logic, you can translate it almost mechanically to a concept in programming, and visa versa” LamdaDays 2016 Philip Wadler’s keynote on Curry-Howard Isomorphism at LambdaDays 2016 Bartosz’s Curry-Howard-Lambek Isomorphism at LambdaDays 2016 Imposing structure on the universe because that is the only way we can understand stuff Wondering if “mathematics is just the way of studying our minds rather than an objective reality” “If category theory is the study of the human mind, then everything must follow the laws of category” Possibility to take category theory and explain it using examples from other domains Introduction to Category Theory talk as a starting point How useful it is to learn category theory??? “I think that getting this higher-level view […] drives you to better solutions” Importance of keeping your mind open because you never know when something will be useful As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Matthew Butterick. We talk about using Racket as someone who doesn’t consider themselves a developer; the power of Domain Specific Languages; Pollen, a DSL for creating web sites; and his book Beautiful Racket. Our Guest, Matthew Butterick Practical Typography Beautiful Racket Pollen Announcements EuroClojure is coming up in Bratislava, Slovakia from October 25-26. Visit http://euroclojure.org/ to find out more, register, or sign up for their mailing list. The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit http://scala.io/ for more information and to register. CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit http://www.scalawave.io/ to find out more and sign up for their newsletter for updates. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. The 2016 Clojure Conj will be taking place in Austin, TX on December 1st – 3rd. Visit http://2016.clojure-conj.org for more information and to register. Lambda Days will be taking place again on the 9th and 10th of February 2017. Visit www.lambdadays.org to submit your talk and keep updated as more information becomes available. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Matthew Practical Typography Pollen Beautiful Racket Episode 24 with Matthew Flatt Episode 48 with Matthias Felleisen Cognicast with Sam Tobin-Hochstadt Racket Scheme Starting out as a type designer “Maybe I should just write a program to do it” Kerning Just van Rossum Guido van Rossum Python for automating tasks in type design Starting as web designer and frustration with templating languages The pain of XSLT for creating web pages The secret connection of Lisp and XML Scribble Typography for Lawyers Pollen code TeX “Before computers were the technology industry, printing was the technology industry” Quad What was Matthew’s transition to Racket as someone looking for a better tool “Beautiful Racket is the book I wish I could travel through time and give to myself” Why Racket, Why Lisp Hackers and Painters by Paul Graham The idea of an expression based language Knuth’s idea of “You don’t really know anything until you can teach it to a computer” Pollen as a Domain Specific Language What people can expect from Beautiful Racket Dr. Racket DSLs as a problem solving technique “By making it easy to make languages, it makes it cheap to make languages” RacketCon Shill a secure shell scripting language “It’s a tool you can use and don’t need any permission” Finding the magic moment to share ideas “If you want to help yourself, check out Racket” Typography for Lawyers Pollen source Joel Dueck’s Secretary of Foreign Relations Flatland e-book created by Pollen on createspace Flatland Pollen Source “If any of you go out and try Racket and hate it, let me know” Sending message via comments on Beautiful Racket As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Hardy Jones. We talk his enthusiasm for languages, why types, working in teams, trade-offs, and much, much more. Our Guest, Hardy Jones @st58 on Twitter joneshf on Github https://joneshf.github.io/ Magic Read Along Announcements EuroClojure is coming up in Bratislava, Slovakia from October 25-26. Visit http://euroclojure.org/ to find out more, register, or sign up for their mailing list. The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit http://scala.io/ for more information and to register. CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit http://www.scalawave.io/ to find out more and sign up for their newsletter for updates. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. The 2016 Clojure Conj will be taking place in Austin, TX on December 1st – 3rd. Visit http://2016.clojure-conj.org for more information and to register. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Hardy NoRedInk Brian Lonsdorf on Episode 51 Magic Read Along How Hardy got into software Python Haskell RPL Prolog JavaScript “How to work effectively on a team with a lot of people” Learn You a Haskell Haskell: The Craft of Functional Programming What was the spark for being a language enthusiast Learning programming languages compared to learning natural languages What features in languages Hardy is favoring now Types as a languages all to itself Benefits of type systems vs a dynamic functional language Functional JavaScript without enforced purity Value of type system to coordinate changes between teammates “There’s so much more that helps less” Elm Ruby Elixir Folding ideas back in between different languages Trying to stick to the idioms of the language and project one works in “You want to talk lenses, we can talk lenses” Encoding effects into types What are lenses? Prisms Proofs Attempting to bring Proofs to Elm Hardy’s view of the difference between PureScript and Elm PureScript Proofs “It’s not this scary thing” Different levels of proving software “If your function is ‘a -> a’ there is only one implementation of that” Proof examples in Elm Equivalence example vs Equality example “Whatever you’re doing take a step back and try something different” Magic Read Along Episode 11 Magic Read Along Episode 13 As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Scott Wlaschin. We talk his introduction to functional programming and F#, making the ideas accessible without needing a math background, functional programming being similar to object oriented programming taken to the extreme, and much, much more. Our Guest, Scott Wlaschin @ScottWlaschin on Twitter F# for fun and profit Announcements Lambda World will be taking place September 30th & October 1st, 2016. Lambda.World is the longest functional programming conference in Spain and Portugal and one of the biggest in Europe. Visit www.lambda.world to find out more and to register. The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit http://scala.io/ for more information and to register. CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit http://www.scalawave.io/ to find out more and sign up for their newsletter for updates. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Scott F# for fun and profit Ten reasons not to use a statically typed functional programming language F# How Scott got introduced to functional programming Smalltalk Python How Scott got introduced to F# Haskell OCaml Miranda Convenience of getting started in F# Benefit of being on a known platform Immutability Partial Application Yaron Minsky Jane Street Making Illegal States Unrepresentable Learning a language by writing a blog Reluctance to use jargon “I had to translate Haskell into F#” “Why do people care about Monads, Monoids, Applicatives, and all that?” Railway Oriented Programming Difference between giving someone tools vs giving someone a recipe Railway Oriented Programming is really about error handling What are some of the most well received topics from his content for getting started FP Patterns presentation A functional approach to Domain Driven Design Scott’s slide on “Patterns in Functional versus Object Oriented Programming” “How do you do a loop [if you don’t have immutability]?” “The most common functional programming language is Excel macros Organization of F# for fun and profit site F# for fun and profit e-book GitBook Dr Frankenfunctor and the Monadster April Fool’s post of migrating to Scala Scala for fun and profit Understanding fundamentals and patterns Monoids series The Elevated World series Schism between mathematically oriented and humanist sides of programming “[Functional Programming] is not that scary” “Object Oriented design principles taken to the extreme look a lot like Functional Programming.” The Design of Everyday Things Don’t Make Me Think The call to start looking into usability of your applications What is on Scott’s radar “If your young, learn as many languages as possible” Learn how to be a better teacher Dan North’s Accelerating Agile talk As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Morten Kromberg. We talk his introduction to APL, the APL landscape, what the future looks like for APL, resources for getting started, and much more. Our Guest, Morten Kromberg @mkromberg on Twitter About the CXO Announcements PWLConf 2016 is the first full-day Papers We Love conference, co-located with the preconference events at Strange Loop in Saint Louis, Missouri on September 15th. Keep an eye out for updates on pwlconf.org. The Erlang User Conference is coming up in Stockholm, Sweden, the 6th through the 16th of September. Early Bird tickets are now available and get a 10% discount on the conference when you use the code: FunctionalGeekery10 when registering. Lambda World will be taking place September 30th & October 1st, 2016. Lambda.World is the longest functional programming conference in Spain and Portugal and one of the biggest in Europe. Visit www.lambda.world to find out more and to register. The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit http://scala.io/ for more information and to register. CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit http://www.scalawave.io/ to find out more and sign up for their newsletter for updates. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Morten Morten’s introduction to APL 1 2 3 + 4 5 6 “Waiting for APL to dominate the world” A Programming Language by Kenneth Iverson Designed for teaching mathematics and arrays 50th Anniversary of APL coming up What the user-base of APL looks like What makes Morten still smile about using APL after all these years Where APL fits in a application environment Using APL for reading and crunching data APL as a prototyping tool Shape Invariance in APL Optimized internal types Symantec density of APL Dyalog What the future of APL might look like Roger Hui J language Ability to optimize special cases of idiomatic APL John Scholes Point Free APL mean← +/ ÷ ≢ ⍝ “The mean is the sum (plus reduction) divided by the count (tally)” – this juxtaposition of functions is a “points free” or “tacit” form known as a “fork”: (f g h)x ←→ (f x) g (h x), inherited from classical mathematical notation, as in (f+g) x ←→ (f x) + (g x) variance←{mean (⍵-mean ⍵)*2} ⍝ “The variance is the mean of the squares of the differences between each item and the mean of the argument” stddev←{(variance ⍵)*0.5} ⍝ “The standard deviation is the square root of the variance” stddev 600 470 170 430 300 ⍝ 147.3227749 Try APL How to find out more about APL Dyalog Forums Dyalog blog Morten’s Google Talk video.dyalog.apl Conway’s Game of Life in APL Interactive tutorial of Conway’s Game of Life on Try APL British APL Association Vector K programming language Dyalog APL version 15.0 available for non-commercial use 2016 Dyalog User Meeting Functional Conf in Bangalore Morten’s call to action About the CXO Morten’s posts on the Dyalog blog As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Alex Weiner. We talk his introduction to APL, comparison to Assembly and C programming, use in side projects to show examples of APL, discuss the power of APL, getting started with APL, and more. Our Guest, Alex Weiner @alexcweiner on Twitter http://alexweiner.com/ alexweiner@alexweiner.com Announcements Compose Melbourne is a new functional programming conference focused on developing the community and bringing typed functional programming to a wider audience. Visit www.composeconference.org/ to find out more. ElixirConf is taking place August 31st through September 2nd in Orlando, Florida. Visit http://www.elixirconf.com to register and find out more. Full Stack Fest will be hold in Barcelona on September 5-9th. You can check out 2016.fullstackfest.com to find out more. PWLConf 2016 is the first full-day Papers We Love conference, co-located with the preconference events at Strange Loop in Saint Louis, Missouri on September 15th. Keep an eye out for updates on pwlconf.org. The Erlang User Conference is coming up in Stockholm, Sweden, the 6th through the 16th of September. Early Bird tickets are now available and get a 10% discount on the conference when you use the code: FunctionalGeekery10 when registering. Lambda World will be taking place September 30th & October 1st, 2016. Lambda.World is the longest functional programming conference in Spain and Portugal and one of the biggest in Europe. Visit www.lambda.world to find out more and to register. The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit http://scala.io/ for more information and to register. CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit http://www.scalawave.io/ to find out more and sign up for their newsletter for updates. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Alex APL Conway’s Game of Life in APL A Programming Language How Alex got into APL Background in Electrical Engineering Sticking to the classic math symbols Math background of APL Teaching Linear Algebra “This should be writable on a whiteboard” Learning APL from “masters” on the job Similarities and differences between thinking in APL vs Assembly and C Infix operators “Already the math I knew” Where APL is a benefit Image Processing in APL Parsing HTTP response in APL Map and Each in APL Max example – ⌈/ 1 7 3 9 2 5 Epsilon example – 3 5 7 9 10 ∊ 7 Various APL Examples FizzBuzz example in APL “What’s the qualities you want in this list” What excites Alex about APL How much does APL lead to complex solutions? “You will meet all of us very quickly” Resources for people to start learning APL Dyalog tryapl.org Mastering Dyalog APL J language APL to J dictionary GNU APL J’s relation to APL Dyalog ’16 As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Yan Cui. We talk his introduction to functional programming via Erlang and F#, getting functional languages adopted in a company, type providers, we wrap up with a rundown of a number of different languages, and much more in between. Our Guest, Yan Cui @theburningmonk on Twitter http://theburningmonk.com/ Announcements Compose Melbourne is a new functional programming conference focused on developing the community and bringing typed functional programming to a wider audience. Visit www.composeconference.org/ to find out more. ElixirConf is taking place August 31st through September 2nd in Orlando, Florida. Visit http://www.elixirconf.com to register and find out more. Full Stack Fest will be hold in Barcelona on September 5-9th. You can check out 2016.fullstackfest.com to find out more. PWLConf 2016 is the first full-day Papers We Love conference, co-located with the preconference events at Strange Loop in Saint Louis, Missouri on September 15th. Keep an eye out for updates on pwlconf.org. The Erlang User Conference is coming up in Stockholm, Sweden, the 6th through the 16th of September. Early Bird tickets are now available and get a 10% discount on the conference when you use the code: FunctionalGeekery10 when registering. Lambda World will be taking place September 30th & October 1st, 2016. Lambda.World is the longest functional programming conference in Spain and Portugal and one of the biggest in Europe. Visit www.lambda.world to find out more and to register. Scala Wave is coming up on the 14th and 15th of October in Gdańsk, Poland. Visit http://www.scalawave.io/ to find out more and sign up for their newsletter for updates. The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit http://scala.io/ for more information and to register. CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Yan Gamesys Yubl A look at Microsoft Orleans through Erlang-tinted glasses Membase Erlang Tomas Petricek Real-World Functional Programming by Tomas Petricek F# Microsoft Orleans What appealed to Yan about Erlang Message passing in Erlang Alan Kay’s definition of Object Oriented Growing Object Oriented Software, Guided by Tests What appealed to Yan about F# Simon Cousin moving to F# Type system of F# Making legal states unrepresentable in your program Edwin Brady on Episode 54 Getting a junior developer up to speed on F# in two weeks Difference in way of thinking vs syntax between F# and C# Lessons learned introducing F# to a company Type Providers Evelina Gabasova Integration to other languages via Type Providers Overview of what it means to write a Type Provider Michael Newton’s Type Providers from the Ground Up Elm Reactive Extensions Elm Architecture Idris Dependent Types Rust Shared Borrowed Pointers F# Unit of Measure types Mars Climate Orbiter bug Go Implicit interfaces Clojure Macros Elixir Haskell Upcoming appearances Leetspeak 2016 CodeMesh Look at serverless technologies “Learn F#, use F#” Scott Wlaschin’s F# for Fun and Profit As always, a giant Thank You goes to David Belcher for the logo design.

In this episode I talk with Lars Hupel. We talk his introduction to Functional Programming with Haskell, Scala, and move to working on Isabelle for creating theorems about proving your program. Our Guest, Lars Hupel @larsr_h on Twitter Lars online Announcements Compose Melbourne is a new functional programming conference focused on developing the community and bringing typed functional programming to a wider audience. Visit www.composeconference.org/ to find out more. ElixirConf is taking place August 31st through September 2nd in Orlando, Florida. Visit http://www.elixirconf.com to register and find out more. Full Stack Fest will be hold in Barcelona on September 5-9th. You can check out 2016.fullstackfest.com to find out more. PWLConf 2016 is the first full-day Papers We Love conference, co-located with the preconference events at Strange Loop in Saint Louis, Missouri on September 15th. Keep an eye out for updates on pwlconf.org. The Erlang User Conference is coming up in Stockholm, Sweden, the 6th through the 16th of September. Early Bird tickets are now available and get a 10% discount on the conference when you use the code: FunctionalGeekery10 when registering. Lambda World will be taking place September 30th & October 1st, 2016. Lambda.World is the longest functional programming conference in Spain and Portugal and one of the biggest in Europe. Visit www.lambda.world to find out more and to register. The 2016 edition of ScalaIO will take place in Lyon, France, on 27th and 28th of October. Visit http://scala.io/ for more information and to register. CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit codemesh.io to register and submit your talk. Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more. If you have a conference related to functional programming, contact me, and I will be happy to announce it. Topics About Lars How Lars Isabelle Haskell Scala Lars’ first exposure to Haskell from a C and Java background Using Scala as a transition strategy from OOP to FP Importance of feedback on actual code Programming in Scala Writing the Travelling Sales Person problem in Haskell Progression to tooling that assures your program is right Lack of debugger in Haskell and Scala Use of the REPL in Haskell and Scala scalaz Relation of QuickCheck and ScalaCheck to Isabelle What is Isabelle Ability to extract code from Isabelle Isar HOL higher order logic Where Isabelle fits with other theorem proving languages Coq HOL Light Agda Idris What Lars is working on in Isabelle Code generation to x86 machine language Lem Different proving strategies available in Isabelle Interactive Theorem Proving Automated Theorem Proving Tactics Lemmas Relationship between Tactics and Lemmas Programming and Proving Isabelle Archive of Formal Proofs Gödel’s ontological proof Typelevel Lambda World ITP 2016 EPFL Check out Isabelle to know what is possible As always, a giant Thank You goes to David Belcher for the logo design.