Categories
Podcasts

Functional Geekery Episode 79 – Lennart Fridén

In this episode I talk with Lennart Fridén. We talk his entry into Elixir, working to help build the Stockholm Elixir group, his Journeyman Tour, Mob Programming, and more.

Our Guest, Lennart Fridén

@DevLCSC on Twitter
DevL on Github
http://codecoupled.org/

Sponsors

This episode is sponsored by DailyDrip.com. Use the coupon `geekery` to save $9 on your first month, and make learning part of your daily routine with DailyDrip.com.

Announcements

f(by) is coming up on the 10th of December in Minsk, Belarus. Visit http://fby.by to find out more 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.

Kats Conf 2 will be taking place in Dublin, Ireland on the 18th of February. Visit http://www.katsconf.com/ to register and for more information.

ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit www.clojured.de to get tickets and keep updated as more information becomes available.

BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit www.bobkonf.de for more information about the conference.

ElixirDaze is coming up on March 2nd and 3rd. With keynotes by Prag Dave Thomas and Saša Jurić, make sure to visit www.elixirdaze.com for more information and to register.

Destination Code, a new unconference starting in Utah, is having its inaugural event March 27-30th, 2017. Visit http://www.destination.codes/ to find out more.

Erlang & Elixir Factory 2017 is on the 23rd and 24th of March. Visit www.erlang-factory.com/sfbay2017 for more information.

flatMap(Oslo) is a FP-conference with focus on Scala and the JVM, taking place on May 2nd and 3rd in Oslo, Norway. Please go to http://2017.flatmap.no/cfp/ to learn more.

Elm Europe will be taking place June 8th and 9th in Paris, France. Visit http://elmeurope.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 Lennart
Stockholm Elixir Meetup Group
Lennart mini-interview at ElixirConf 2015
How Lennart came to Elixir
C as a high level language coming from Assembly
General enthusiasm around Elixir regardless of when one came from
“There’s an intrinsic fun in going deeper”
Elixir as the language of the year
The Pragmatic Programmer
Erlang on Xen [Ling]
Lennart’s presentation at ElixirConf 2015
Being called up to the Principle’s Office by Björn Gustavsson
Building a community with the Stockholm Elixir group
Go Language
Rust
Clojure
Importance of getting people involved early
“You don’t have to be a Joe Armstrong, or Robert Virding to talk about the language”
Overview of Lennart’s Journeyman Tour
“I got to go in knowing a lot less [than the teams I worked with]”
Lennart’s announcement blog post
Mob Programming
Woody Zuill
“Pair programming on steroids”
Creating a Key-Value store as a mob exercise for a user group meeting
Lennart on Elixir Fountain
Mob Programming sessions to show off Elixir
Mob Programming to spur excitement more than just a presentation
Mob programming as a Trojan Horse […] to show off Elixir
“The more you work with people, the closer you work with people, the more interesting they become”
Klarna
Erlang and Elixir and shared environment and community
LFE (Lisp Flavoured Erlang)
Mob Programming Conference in Boston on April 6th and 7th
Agile Games
Lennart’s Blog
Elixir Conference Europe
Elixir Conference US in Bellevue, Washington
Erlang User Conference

As always, a giant Thank You goes to David Belcher for the logo design.

Categories
Podcasts

Functional Geekery Episode 78 – ‘Ley Missailidis

In this episode I talk with ‘Ley Missailidis. We talk his introduction Erlang and Elixir, Elm, and the pairing of Phoenix and Elm to reduce the complexity of front-end development.

Our Guest, ‘Ley Missailidis

@_polymetis_ on Twitter
polymetis on Github
http://worldoftomorrow.ca

Sponsors

This episode is sponsored by DailyDrip.com. Use the coupon `geekery` to save $9 on your first month, and make learning part of your daily routine with DailyDrip.com.

Announcements

f(by) is coming up on the 10th of December in Minsk, Belarus. Visit http://fby.by to find out more 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.

Kats Conf 2 will be taking place in Dublin, Ireland on the 18th of February. Visit http://www.katsconf.com/ to register and for more information.

ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit www.clojured.de to get tickets and keep updated as more information becomes available.

BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit www.bobkonf.de for more information about the conference.

Destination Code, a new unconference starting in Utah, is having its inaugural event March 27-30th, 2017. Visit http://www.destination.codes/ to find out more.

Erlang & Elixir Factory 2017 is on the 23rd and 24th of March. Visit www.erlang-factory.com/sfbay2017 for more information.

flatMap(Oslo) is a FP-conference with focus on Scala and the JVM, taking place on May 2nd and 3rd in Oslo, Norway. Please go to http://2017.flatmap.no/cfp/ to learn more.

Elm Europe will be taking place June 8th and 9th in Paris, France. Visit http://elmeurope.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 ‘Ley
Erlang
iwantmyname
RabbitMQ
Chicago Boss
Elixir
‘Ley’s transition from JavaScript to Erlang
CoffeeScript
Learn You Some Erlang
D3.js
Migrating to Elixir
Erlang Factory 2014
Chris McCord’s Presentation at Erlang Factory 2014
ElixirConf 2014
Dynamo
Ecto
Looking for a better way to manage the front end piece of applications
Phoenix Framework
Elm
Elixir Conf US 2015
Alan Gardner’s Phoenix and Elm talk
Elm code as another module in Phoenix
Alan Gardner’s Phoenix and Elm blog series
“I managed to code the entire thing with help and error messages without looking online”
Thinking in The Elm Architecture as a game loop or movie frames
Subscriptions in Elm 0.17
Frank Bonetti’s Elm Phoenix Socket Library
Appeal of the Channels abstraction in Phoenix
How ‘Ley structures Phoenix and Elm applications
Evan and Chris talk on Phoenix and Elm at Erlang Factory 2016
Alan Gardner’s Example App on Github
Elm in Action
Rock-Paper-Scissors in Elm
Elixir in Action
Dialyzer
“Sometimes in Elixir it is easier just to drop into Erlang”
“Beware of over-dumping into Erlang if you are trying to solve a problem”
iwantmyname blog
iwantmyname’s post on FreeBSD, ZFS, and Elixir and Phoenix

*** Addendum from ‘Ley after the episode

Elm S3 uploading with Elxir backend

As always, a giant Thank You goes to David Belcher for the logo design.

Categories
Podcasts

Functional Geekery Episode 77 – Jared Roesch

In this episode I talk with Jared Roesch. We talk his history of functional programming, work on the Rust compiler, dependent types, the Lean Proving Language, and much, much more.

Our Guest, Jared Roesch

@roeschinc on Twitter
jroesch on Github

Sponsors

This episode is sponsored by DailyDrip.com. Use the coupon `geekery` to save $9 on your first month, and make learning part of your daily routine with DailyDrip.com.

Announcements

f(by) is coming up on the 10th of December in Minsk, Belarus. Visit http://fby.by to find out more 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.

Kats Conf 2 will be taking place in Dublin, Ireland on the 18th of February. Visit http://www.katsconf.com/ to register and for more information.

ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit www.clojured.de to get tickets and keep updated as more information becomes available.

BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit www.bobkonf.de for more information about the conference.

Destination Code, a new unconference starting in Utah, is having its inaugural event March 27-30th, 2017. Visit http://www.destination.codes/ to find out more.

Erlang & Elixir Factory 2017 is on the 23rd and 24th of March. Visit www.erlang-factory.com/sfbay2017 for more information.

flatMap(Oslo) is a FP-conference with focus on Scala and the JVM, taking place on May 2nd and 3rd in Oslo, Norway. Please go to http://2017.flatmap.no/cfp/ to learn more.

If you have a conference related to functional programming, contact me, and I will be happy to announce it.

Topics

About Jared
Lean Theorem Prover
How Jared got into software development
How Jared was first exposed to functional programming
Haskell
Scala
Clojure
Ruby
How learning functional programming affected daily work in Ruby and Rails
What captured Jared’s interest in typed languages
Rust
POPL – Principles of Programming Languages
Jared’s work with Rust
Rust’s ability to support functional programming concepts
“A love child between Haskell and C++”
Rust’s support for scoped mutation of data
Type classes and traits in Rust
ASPLOS – Architectural Support for Programming Languages and Operating Systems
Idris
Verified pacemaker on functional architecture chip
FPGA – Field-programmable gate array
Jared’s introduction to dependent types
Software Foundations
Certified Programming with Dependent Types
Coq
General lack of tooling for getting started in dependent type languages
Type-driven Development with Idris
Formal Reasoning About Programs
Intrinsic vs extrinsic proofs with dependent types
Dependent types and their relation, or not, to functional programming
Nuprl
JonPRL
F*
Lean
The goal of making dependent types accessible with Lean
Z3 SMT solver
The 30,000 foot view and philosophy of Lean
Scripting Lean in Lean
Theorem Proving in Lean
eBPF – Extended Berkeley Packet Filter
Provable eBPF compilation
Target of Lean
Dafny
Project Everest

As always, a giant Thank You goes to David Belcher for the logo design.

*** Update January 18th ***
Typed Coin

Categories
Podcasts

Functional Geekery Episode 76 – Anthony Cipriano

In this episode I talk with Anthony Cipriano. We talk his introduction to functional programming, APL, J, K, the path to writing AntLang, why AntLang, where AntLang took as its inspiration, and more.

Our Guest, Anthony Cipriano

@_AntLang on Twitter
https://antlang-software.github.io/
AntLang on Github
AntLang channel on YouTube

Sponsors

This episode is sponsored by DailyDrip.com. Use the coupon `geekery` to save $9 on your first month, and make learning part of your daily routine with DailyDrip.com.

Announcements

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.

F(by) is coming up on the 10th of December in Minsk, Belarus. Visit http://fby.by to find out more and to register.

ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit www.clojured.de to get tickets and keep updated as more information becomes available.

BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit www.bobkonf.de for more information about the conference.

Destination Code, a new unconference starting in Utah, is having its inaugural event March 27-30th, 2017. 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 Anthony
AntLang
How Anthony got into programming
Prolog
“[Prolog] isn’t a different kind of language when you learn it first”
Erlang
WhatsApp
Starting to write a Lisp in Erlang to learn writing a language
Haskell
APL
“You can type in `1 2 3 + 4 5 6` and spits out three numbers”
“People who learn APL absolutely love it or hate it”
tryapl.org
Writing APL on paper and compiling in head
J language
Android mobile version of J
K language
Kona
Translating APL to J
“The compiler in my mind has a better compiler than J does”
Errors as generic “Domain Error”
What started the desire to write AntLang
Implementations of interpreters for AntLang
Happy for text parsing
Perl 6
What kind of problem domains is AntLang targeting
What does the future look like for AntLang
How K and AntLang are related
Simplicity of AntLang as a selling point
“If someone has the question ‘Why AntLang?”, well ‘Why not?'”
AntLang embedded in Perl
“Look at the source code and see how small it is”
Resources for AntLang
AntLang Tutorials on YouTube
Essential AntLang

As always, a giant Thank You goes to David Belcher for the logo design.

Categories
Podcasts

Functional Geekery Episode 75 – Eric B. Merritt

In this episode I talk with Eric Merritt. We catch up on his experience with unikernels, containers, Nix, microservices, the benefits of orchestration platforms to allow developers to focus on solving the business problems, and much, much more.

Our Guest, Eric B. Merritt

@ericbmerritt on Twitter
http://blog.ericbmerritt.com/

Sponsors

This episode is sponsored by DailyDrip.com. Use the coupon `geekery` to save $9 on your first month, and make learning part of your daily routine with DailyDrip.com.

Announcements

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.

F(by) is coming up on the 10th of December in Minsk, Belarus. Visit http://fby.by to find out more and to register.

ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit www.clojured.de to get tickets and keep updated as more information becomes available.

BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit www.bobkonf.de for more information about the conference.

Destination Code, a new unconference starting in Utah, is having its inaugural event March 27-30th, 2017. 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 Eric
Eric on Episode 20
Unikernels
Unikernels are a Perfect Diamond vs Worse is Better of containers
Lisp: Good News, Bad News, How to Win Big
Section 2.1 The Rise of Worse is Better
Docker
NixOS
Kubernetes
How the old programming rules don’t apply
Platform Engineers and Business Application Engineer
AWS Elastic Beanstalk
OCaml
Haskell
Scala
A new way of getting Erlang’s concurrency model
How communication between microservices is setup when not using Erlang
Writing microservices in Haskell
Writing microservices in Scala
Platforms as tooling compared to Garbage Collection or Algebraic Data Types
Consul
HashiCorp
Docker Swarm
Moving to platform services and containers
“By allowing your engineers to focus on your business and offloading and removing the risk in developing your own platform your reducing your risk to make that transition”
Nix Package Manager
Ability to rebuild host at any point in time
Building containers using Nix expressions
NixOS
Running NixOS on your laptop
Resources for getting started with Nix
Start with using Nix Package manager on your laptop
Nix Manual
ArchLinux
Run NixOS on your laptop or AWS
Opportunities opened up for trying out and introducing a new language
Getting a side project in Haskell running in a container in production in a couple of hours
“Getting started is so much easier than it used to be”

As always, a giant Thank You goes to David Belcher for the logo design.

Categories
Podcasts

Functional Geekery Episode 74 – Zeeshan Lakhani

In this episode I talk with Zeeshan Lakhani. We talk his introduction to functional programming, Clojure, Erlang, distributed systems, session types, Papers We Love, and much more.

Our Guest, Zeeshan Lakhani

@zeeshanlakhani on Twitter
Papers We Love
@papers_we_love on Twitter

Sponsors

This episode is sponsored by DailyDrip.com. Use the coupon `geekery` to save $9 on your first month, and make learning part of your daily routine with DailyDrip.com.

Announcements

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 get tickets and keep updated as more information becomes available.

BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit www.bobkonf.de for more information about the conference.

If you have a conference related to functional programming, contact me, and I will be happy to announce it.

Topics

About Zeeshan
Papers We Love
LambdaConf 2015 episode of Functional Geekery with Zeeshan
How Zeeshan got into functional programming
Clojure
StrangeLoop 2012
Programming Languages Coursera course by Dan Grossman
Basho
Erlang
Racket
Scheme
Transitioning to Clojure
“Getting more into context”
MATLAB
“Clojure changed my mindset of how I deliver programs”
Making the change to working with Erlang
Distributed Systems
ElasticSearch
RabbitMQ
Thinking of everything as a process
test.check
schema-gen
Quviq
QuickCheck for Erlang
Thinking in state machines
Pattern matching
Erlang Factory
Racket as a language about writing languages
Lasp from Christopher Meiklejohn
Oregon Programming Languages Summer School
Zeeshan’s Erlang Type System talk at Erlang Factory
Data Flow Semantics paper from Google
Pony
GenStage in Elixir
Session Types
Zeeshan’s Intro to Sessions Types at MoonConf
Scribble
ABCD group
Professor Wadler on Episode 39 talking Session Types
Papers We Love
Papers We Love guidelines
StrangeLoop
Papers We Love Conf
Attending a Papers We Love and format
“Computing is not about factions, but about the universality of it”
Papers We Love Github repository
Papers We Love YouTube channel
New York Chapter of Papers We Love

As always, a giant Thank You goes to David Belcher for the logo design.

Categories
Podcasts

Functional Geekery Episode 73 – Jonas Bonér

In this episode I talk with Jonas Bonér. We talk his introduction to Scala, the Actor Model, Akka, Reactive Programming, Microservices, Distributed Systems, and more.

Our Guest, Jonas Bonér

jonasboner.com
@jboner on Twitter
Lightbend

Announcements

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 get tickets and keep updated as more information becomes available.

BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit www.bobkonf.de for more information about the conference.

If you have a conference related to functional programming, contact me, and I will be happy to announce it.

Topics

About Jonas
Lightbend
AspectWerkz
AspectJ
Akka
How Jonas got into software
C++
Java
Erlang
Prolog
Scala
Actors library in Scala
Akka
Motivation for choosing Scala
Two different tracks of Scala
“Akka and Erlang are very Object-Oriented”
Actors library and motivation to create Akka
Supervision model
Comparison of Erlang’s vs Akka’s Actor Models
What benefits the JVM provides
Scala 2.12
Traits in Scala
Single Abstract Methods types and Lambdas
Types and Actors
become in Akka
Type Channels
Akka Streams
Akka Typed
Akka Clustering
Event Sourcing library for Akka
Apache Camel Project
Alpakka
Reactive systems
Reactive Manifesto
Functional Reactive Programming
Rx Java and Reactive Extensions in .NET
“Failure is a regular state in the application life-cycle”
Back-pressure
Reactive Streams Specification
Data as streams
Distributed Systems
Jonas’ talk at Reactive Summit
Microservices from an Actor Model perspective
“You can easily create a Distributed Monolith”
Falling back to thinking in synchronous communication
“If your microservices aren’t truly isolated they can’t be resilient”
Embrace the Network
Decoupling microservices in Time and Space
“Message passing should be the default for all distributed computing”
Using REST as an optimization
Kafka for storing messages
Theron
Akka Actor Refs
Going all in on asynchronous message passing
Resources for getting a better understanding of distributed systems
Reactive Microservices Architecture
Lightbend
Lightbend blog
Akka.io
Akka blog
jonasboner.com

As always, a giant Thank You goes to David Belcher for the logo design.

Categories
Podcasts

Functional Geekery Episode 72 – Gabriel Gonzalez

In this episode I talk with Gabriel Gonzalez. We cover numerous topics around Haskell from stumbling blocks for beginners, to co-routines, to shell scripting with Haskell, to equational reasoning, and much, much more.

Our Guest, Gabriel Gonzalez

http://www.haskellforall.com/
@GabrielG439 on Twitter
Tekmo on Reddit

Announcements

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 get tickets and keep updated as more information becomes available.

BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit www.bobkonf.de for more information about the conference.

If you have a conference related to functional programming, contact me, and I will be happy to announce it.

Topics

About Gabriel
Tekmo on Reddit
Gabriel on Haskell Cast
How Gabriel got into programming
How Gabriel got into Haskell
Poll for Haskell logo
Ph.D.
Haskell as an alternative to shell scripting
Need of a compelling project to learn Haskell
Refactoring/re-architecting in Haskell
“People who are willing to make mistakes and write messy code in Haskell are the ones who learn it the most quickly”
Composability in Haskell
Difference between sub-routines and functions
Equational Reasoning
Peter Landin’s The Next 700 Programming Languages
Larger Right-Hand Sides
Hurdles seen for people getting into Haskell
Cultivating motivation
Current stumbling blocks for new users to Haskell
Haskell Programming From First Principles
Stephen Diehl’s What I Wish I Knew When Learning Haskell
Pipes
Co-routines
Laziness in Haskell
Turtle Project
Shell scripting in Haskell
Using shell scripting as a low-barrier way to learn Haskell
Turtle.Tutorial module
“No actual Monad Enlightenment”
“Haskell promotes good practices by discouraging things you shouldn’t be doing a lot of anyway”
Lessons taken away from Haskell when going back to other languages
Making impossible states unrepresentable
State of the Haskell Ecosystem
LambdaConf Retreat
Bench Library
Dhall Language
Work on improving the state of IDE plugins
Haskell for Mac
Leksah
IDE Support from the State of the Haskell Ecosystem

As always, a giant Thank You goes to David Belcher for the logo design.

Categories
Podcasts

Functional Geekery Episode 71 – Nikhil Swamy

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.

Categories
Podcasts

Functional Geekery Episode 70 – Simon Thompson

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.