The Heartbleed Bug.

The Heartbleed Bug in Haskell

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

True is a bad argument

λ> takeWord16 True text

<interactive>: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

λ>  takeWord16 10 text
"Niki\33624\5479\SOH\NUL\60480\5115"

Partial Functions

λ> :t head
head :: [a] -> a

λ> head "CUFP"
'C'

λ> head []
*** Exception: Prelude.head: empty list

Functional Correctness

λ> fib 1 <= fib 42
False

λ> mapReduce 42 sum (+) [1..20]
0 

Goal: Extend Type System

• To prevent wider class of errors

• To enforce program specific properties

Plan

Follow online http://goto.ucsd.edu/~nvazou/presentations/cufp16/01-index.html

1. Refinements Types
2. Data Types
3. Termination
4. Reflection
5. Structural Induction
6. Case Study: MapReduce

Evaluation

• Diverse Code Bases

• 10KLoc / 56 Modules

• Memory Safety, Termination, Functional Correctness

Inference is Crucial

Evaluation

• Specifications: 1 / 10 LOC (ok)

• Compile Time: 1s / 10 LOC (not ok!)

Conclusion

Refinement Types: Automated Dependent Typing via SMT

Thank You!

cabal install liquidhaskell
http://www.refinement-types.org
online demo @ http://goto.ucsd.edu/liquidhaskell