Eliminating Bugs with Dependent Haskell (Experience Report)
Using dependent types in production code is a practical way to eliminate errors. While there are many examples of using dependent Haskell to prove invariants about code, few of these are applied to large scale production systems. Critics claim that dependent types are only useful in toy examples and that they are impractical for use in the real world. This experience report analyzes real world examples where dependent types have enabled us to find and eliminate bugs in production Haskell code.
I work for Facebook in the Programming Languages and Runtimes group. My current projects involve adding capabilities to the Hack programming language that will allow us to guarantee the privacy of user data. In the past, I have also worked on large scale production systems implemented in Haskell.
Before working at Facebook, I was an undergrad at the University of Pennsylvania. During my time at Penn, I worked on a project to verify the type safety System FC using the Coq Proof Assistant. This project was advised by Stephanie Weirich and Richard Eisenberg.
Fri 28 AugDisplayed time zone: Eastern Time (US & Canada) change
14:30 - 16:00 | |||
14:30 30mTalk | Staged Sums of Products Haskell Matthew Pickering University of Bristol, UK, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, UK DOI | ||
15:00 30mTalk | Eliminating Bugs with Dependent Haskell (Experience Report) Haskell Noam Zilberstein Facebook, USA DOI | ||
15:30 30mTalk | Stitch: The Sound Type-Indexed Type Checker (Functional Pearl) Haskell Richard A. Eisenberg Tweag I/O DOI File Attached |