{#ASda} ======== Evaluation ---------- Evaluation ========== LiquidHaskell Is For Real -------------------------
Substantial code bases.
Complex properties.
Inference is crucial.
Numbers -------
**Library** **LOC** --------------------------- --------- `Data.List` 814 `Data.Set.Splay` 149 `Data.Vector.Algorithms` 1219 `Data.Map.Base` 1396 `Data.Text` 3125 `Data.Bytestring` 3501 **Total** **10224** --------------------------- ---------
Numbers -------
**Library** **LOC** **Time** --------------------------- --------- ---------- `Data.List` 814 52s `Data.Set.Splay` 149 26s `Data.Vector.Algorithms` 1219 196s `Data.Map.Base` 1396 247s `Data.Text` 3125 809s `Data.Bytestring` 3501 549s **Total** **10224** **1880s** --------------------------- --------- ----------
Termination ----------- Proving termination is **easy in practice**.
-
`503` recursive functions
-
`67%` automatically proved
-
`30%` need *witnesses* `/[...]`
-
`1` witness per `100` lines of code
-
`20` *not proven* to terminate
-
`12` *do not* terminate (e.g. top-level `IO` loops)
-
`8` currently *outside scope* of LiquidHaskell
Future Work -----------

-
Speed
-
Case Studies
-
**Error Messages**
{#asd} ======= Thank You! ----------
`cabal install liquidhaskell`
`https://github.com/ucsd-progsys/liquidhaskell`