00_Motivation.lhs

Well-Typed Programs Can Go Wrong
================================

 {#asd}
-------



<div class="hidden">

\begin{code}
main = putStrLn "Easter Egg: to force Makefile"
\end{code}

</div>


Division By Zero
----------------




<div class="fragment"> 
\begin{spec}
λ> let average xs = sum xs `div` length xs

λ> average [1,2,3]
2
\end{spec}
</div>

<br>

<div class="fragment"> 
\begin{spec}  
λ> average []
*** Exception: divide by zero
\end{spec}

</div>

Missing Keys
------------

<div class="fragment"> 
\begin{spec}  
λ> :m +Data.Map 
λ> let m = fromList [ ("haskell", "lazy")
                    , ("pyret"  , "eager")]

λ> m ! "haskell"
"lazy"
\end{spec}
</div>

<br>

<div class="fragment"> 
\begin{spec}
λ> m ! "racket"
"*** Exception: key is not in the map
\end{spec}
</div>

Segmentation Faults
-------------------

<div class="fragment"> 
\begin{spec}
λ> :m +Data.Vector 
λ> let v = fromList ["haskell", "pyret"]
λ> unsafeIndex v 0
"haskell"
\end{spec}
</div>

<div class="fragment"> 
<br>
\begin{spec} 
λ> V.unsafeIndex v 3


'ghci' terminated by signal SIGSEGV ...
\end{spec}
</div>


"HeartBleeds"
-------------

\begin{spec}
λ> :m + Data.Text Data.Text.Unsafe 
λ> let t = pack "Shriram"
λ> takeWord16 5 t
"Shrir"
\end{spec}

<br>

<div class="fragment"> 
Memory overflows **leaking secrets**...

<br>

\begin{spec}
λ> takeWord16 20 t
"Shriram\1912\3148\SOH\NUL\15928\2486\SOH\NUL"
\end{spec}
</div>

Goal
----

Extend Type System

<br>

+ To prevent *wider class* of errors

+ To enforce *program specific* properties 


Algorithmic Verification
========================


Tension
-------

<img src="../img/tension0.png" height=300px>

Automation vs. Expressiveness

Tension
-------

<img src="../img/tension1.png" height=300px>

Extremes: Hindley-Milner vs. CoC

Tension
-------

<img src="../img/tension2.png" height=300px>

Trading off Automation for Expressiveness

Tension
-------

<img src="../img/tension3.png" height=300px>

**Goal:** Find a sweet spot?

<!-- BEGIN CUT

Program Logics
--------------

<br>

**Floyd-Hoare** (ESC, Dafny, SLAM/BLAST,...)

<br>

+ **Properties:**   Assertions & Pre- and Post-conditions

+ **Proofs:**       Verification Conditions proved by SMT

+ **Inference:**    Abstract Interpretation

<br>

<div class="fragment"> Automatic but **not** Expressive </div>


Program Logics
--------------

<br>

**Floyd-Hoare** (ESC, Dafny, SLAM/BLAST,...)


<br>

Automatic but **not** Expressive

<br>

+ Rich Data Types ?

+ Higher-order functions ?

+ Polymorphism ?


Refinement Types
----------------

<br>

Generalize *Program Logics* with *Types*

<div class="fragment"> 
<br>

+ **Properties:**  Types + Predicates

+ **Proofs:**      Subtyping + Verification Conditions

+ **Inference:**   Hindley-Milner + Abstract Interpretation

</div>

<div class="fragment"> 
  <br>
  Towards reconciling Automation and Expressiveness
</div>

END CUT -->

Refinement Types
----------------

<br>
<br>

[[continue]](01_SimpleRefinements.lhs.slides.html)