Eliminating Bugs with Dependently Typed Haskell
YOW! Lambda Jam 2021
Using dependent types in production Haskell 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 talk analyzes real world examples where dependent types have enabled us to find and eliminate bugs in production Haskell code.
Noam is a computer scientist interested in programming languages, dependent types, formal verification, functional programming, and static analysis. His goal is to reimagine software engineering by creating a new generation of programming languages and tools that allow developers to think at a higher level and provide stronger static correctness guarantees. He is currently a Staff Software Engineer in the Facebook Programming Languages and Runtimes group and is working on various projects related to the Hack programming language. This work will help thousands of Facebook engineers write safer and more correct code.