18: {x2 : (IO ()) | (x2 == Main.main)}main = [Char] -> (IO ())putStrLn {x2 : [Char] | ((len x2) >= 0)}"Easter Egg: to force Makefile"
Substantial code bases.
Complex properties.
| 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 |
| 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 |
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
cabal install liquidhaskell
https://github.com/ucsd-progsys/liquidhaskell