Liquid Haskell:
Verification of Haskell Code

Niki Vazou
(University of Maryland)

Haskell is SAFE!

Lambda Man.

Fact Check: Buffer Overflows

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

True is a bad argument

λ> takeWord16 True text :5:12: 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 "hat\33624\5479\SOH\NUL\60480\5115\5479"

Goal: Extend Type System

  • To prevent wider class of errors

  • To enforce program specific properties


Installation & Resources