Solid Code with Liquid Types!

Are you tired of writing tests only to see production crash at 5:00pm on a Friday? Traditional type systems can save you from adding an integer to a string but can they save you from being fired? We intoduce Liquid Haskell (don't worry, no previous Haskell knowledge is required) a tool to definitively prove that your code does what you want, no tests needed!

Workshop Plan

Part one:

• Brief Haskell intro (syntax, map/fold/zip)
• Introduction to refinement and liquid types Simple real-world examples (e.g., safe zipping, aggregations)
• Using polymorphism with refinement types (map, zipWith)
• Proving functional equivalence via reflection and PLE

Part two:

Two possible tracks depending on audience progress:

• Track A: Continue with smaller, guided exercises to reinforce basics
• Track B: Interactive project: develop a small programming language and verify key properties like type checking or compilation correctness Advanced attendees may optionally pursue Track B independently even if the group stays with Track A.

Requirements for attendees

Technical Requirements

We will use Liquid Haskell through the web interface at https://liquidhaskell.goto.ucsd.edu/index.html so the attendees will only need to come with a laptop with a web browser installed; still, we recommend using a local installation of Haskell & Liquid Haskell instead.

Knowledge Prerequisites

Basic functional programming knowledge, maps, folds, ecc..

Target Audience

Functional programmers (beginners or intermediate), type system enthusiasts, Haskell users, and anyone interested in formal methods or software verification.

Companies using this technology

Tweag, Well-Typed, Entrans, etc.