Liquid Haskell:
Verification of Haskell Code

Niki Vazou

(University of Maryland)

Liquid Haskell: Verification of Haskell Code

Motivation: Why verification?

Software bugs are Everywhere

“Airbus A400M crashed due to a software bug.”

— May 2015


Software bugs are Everywhere

Heartbleed: a security bug in the OpenSSL cryptography library.”

— April 2014

The Heartbleed Bug.

How The Heartbleed Bug Works

How The Heartbleed Bug Works

Goal: Make Bugs Difficult to Express

Using Modern Programming Languages (e.g., Haskell, Scala, Ocaml, F#).

Because of Strong Types & Lambda Calculus.

Via compile-time sanity checks

Lambda Man.

Fact Check: Haskell VS. Heartbleed

Haskell vs Heartbleed

The Heartbleed Bug in Haskell

λ> :m +Data.Text Data.Text.Unsafe
λ> let text = pack "hat"
λ> :t takeWord16
    takeWord16 :: Int -> Text -> Text

True is a bad argument

λ> takeWord16 True text

    Couldn't match expected type ‘Int’ with actual type ‘Bool’
    In the first argument of ‘takeWord16’, namely ‘True’
    In the expression: takeWord16 True text

But, 10 is a good argument

Reveal 7 extra characters...
λ>  takeWord16 10 text

More Bugs: Program Equivalence

λ> sum  [1..1000]

λ> psum [1..1000]

Goal: Extend Type System

  • To prevent wider class of errors

  • To enforce program specific properties


  1. Refinements Types
  2. Data Types
  3. Termination
  4. Refinement Reflection
  5. Case Study: Verification MapReduce