We’ve taught LiquidHaskell a new trick that we call ``Refinement Reflection’’ which lets us turn Haskell into a theorem prover capable of proving arbitrary properties of code. The key idea is to reflect the code of the function into its output type, which lets us then reason about the function at the (refinement) type level. Lets see how to use refinement types to express a theorem, for example that fibonacci is a monotonically increasing function, then write plain Haskell code to reify a paper-and-pencil-style proof for that theorem, that can be machine checked by LiquidHaskell.
38: {-@ LIQUID "--higherorder" @-} 39: {-@ LIQUID "--totality" @-} 40: module RefinementReflection where 41: import Language.Haskell.Liquid.ProofCombinators 42: 43: fib :: Int -> Int 44: propPlusComm :: Int -> Int -> Proof 45: propOnePlueOne :: () -> Proof 46: fibTwo :: () -> Proof 47: fibCongruence :: Int -> Int -> Proof 48: fibUp :: Int -> Proof 49: fibTwoPretty :: Proof 50: fibThree :: () -> Proof 51: fMono :: (Int -> Int) 52: -> (Int -> Proof) 53: -> Int 54: -> Int 55: -> Proof 56: fibMono :: Int -> Int -> Proof 57:
Shallow vs. Deep Specifications
Up to now, we have been using Liquid Haskell to specify and verify “shallow”
specifications that abstractly describe the behavior of functions. For example,
below, we specify and verify that fibrestricted to natural numbers, always
terminates returning a natural number.
70: {-@ fib :: i:Nat -> Nat / [i] @-} 71: {v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0}fib {v : GHC.Types.Int | v >= 0}i | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 0 = 0 72: | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 1 = 1 73: | otherwise = {v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2)
In this post we present how refinement reflection is used to verify
“deep” specifications that use the exact definition of Haskell functions.
For example, we will prove that the Haskell fib function is increasing.
Propositions
To begin with, we import ProofCombinators, a (Liquid) Haskell library that defines and manipulates logical proofs.
89: import Language.Haskell.Liquid.ProofCombinators
A Proof is a data type that carries no run time information
95: type Proof = ()
but can be refined with desired logical propositions.
For example, the following type states that 1 + 1 == 2
102: {-@ type OnePlusOne = {v: Proof | 1 + 1 == 2} @-}
Since the v and Proof are irrelevant, we may as well abbreviate
the above to
109: {-@ type OnePlusOne' = { 1 + 1 == 2 } @-}
As another example, the following function type declares
that for each x and y the plus operator commutes.
117: {-@ type PlusComm = x:Int -> y:Int -> {x + y == y + x} @-}
Trivial Proofs
We prove the above theorems using Haskell programs.
The ProofCombinators module defines the trivial proof
129: trivial :: Proof 130: trivial = ()
and the “casting” operator (***) that makes proof terms look
nice:
137: data QED = QED 138: 139: (***) :: a -> QED -> Proof 140: _ *** _ = ()
Using the underlying SMT’s knowledge on linear arithmetic, we can trivially prove the above propositions.
147: {-@ propOnePlueOne :: _ -> OnePlusOne @-} 148: () -> {VV : () | 1 + 1 == 2}propOnePlueOne _ = {v : Language.Haskell.Liquid.ProofCombinators.QED | v == Language.Haskell.Liquid.ProofCombinators.QED}trivial *** QED 149: 150: {-@ propPlusComm :: PlusComm @-} 151: x1:GHC.Types.Int -> x2:GHC.Types.Int -> {VV : () | x1 + x2 == x2 + x1}propPlusComm _ _ = {v : Language.Haskell.Liquid.ProofCombinators.QED | v == Language.Haskell.Liquid.ProofCombinators.QED}trivial *** QED
We saw how we use SMT’s knowledge on linear arithmetic to trivially prove arithmetic properties. But how can we prove ``deep’’ properties on Haskell’s functions?
Refinement Reflection
Refinement Reflection allows deep specification and verification by reflecting the code implementing a Haskell function into the function’s output refinement type.
Refinement Reflection proceeds in 3 steps: definition, reflection, and application.
Consider reflecting the definition of fib into the logic
171: {-@ reflect fib @-}
then the following three reflection steps will occur.
Step 1: Definition
Reflection of the Haskell function fib defines in logic
an uninterpreted function fib that satisfies the congruence axiom.
In the logic the function fib is defined.
185: fib :: Int -> Int
SMT only knows that fib satisfies the congruence axiom.
191: {-@ fibCongruence :: i:Nat -> j:Nat -> {i == j => fib i == fib j} @-} 192: x1:{v : GHC.Types.Int | v >= 0} -> x2:{v : GHC.Types.Int | v >= 0} -> {VV : () | x1 == x2 => fib x1 == fib x2}fibCongruence _ _ = {v : Language.Haskell.Liquid.ProofCombinators.QED | v == Language.Haskell.Liquid.ProofCombinators.QED}trivial *** QED
Other than congruence, SMT knowns nothing for the function fib,
until reflection happens!
Step 2: Reflection
As a second step, Liquid Haskell connects the Haskell function fib
with the homonymous logical function,
by reflecting the implementation of fib in its result type.
The result type of fib is automatically strengthened to the following.
210: fib :: i:Nat -> {v:Nat | v == fib i && v = fibP i }
That is, the result satisfies the fibP predicate
exactly reflecting the implementation of fib.
217: fibP i = if i == 0 then 0 else 218: if i == 1 then 1 else 219: fin (i-1) + fib (i-2)
Step 3: Application
With the reflected refinement type,
each application of fib automatically unfolds the definition of fib
once.
As an example, applying fib to 0, 1, and 2 allows us to prove that fib 2 == 1:
231: {-@ fibTwo :: _ -> { fib 2 == 1 } @-} 232: () -> {VV : () | fib 2 == 1}fibTwo _ = {v : [GHC.Types.Int] | null v <=> false}[{v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0, {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1, {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2] *** QED
Though valid, the above fibTwo proof is not pretty!
Structuring Proofs
To make our proofs look nice, we use combinators from
the ProofCombinators library, which exports a family
of operators (*.) where * comes from the theory of
linear arithmetic and the refinement type of x *. y
- requires that
x *. yholds and - ensures that the returned value is equal to
x.
For example, (==.) and (<=.) are predefined in ProofCombinators as
252: (==.) :: x:a -> y:{a| x==y} -> {v:a| v==x} 253: x ==. _ = x 254: 255: (<=.) :: x:a -> y:{a| x<=y} -> {v:a| v==x} 256: x <=. _ = x
Using these predefined operators, we construct paper and pencil-like proofs
for the fib function.
263: {-@ fibTwoPretty :: { fib 2 == 1 } @-} 264: {VV : () | fib 2 == 1}fibTwoPretty 265: = {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2 266: GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0 267: *** QED
Because operator
To allow the reuse of existing proofs, ProofCombinators defines the because
operator (∵)
279: (∵) :: (Proof -> a) -> Proof -> a 280: f ∵ y = f y
For example, fib 3 == 2 holds because fib 2 == 1:
286: {-@ fibThree :: _ -> { fib 3 == 2 } @-} 287: () -> {VV : () | fib 3 == 2}fibThree _ 288: = {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 3 289: GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 290: GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int==. GHC.Types.Int1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1 ∵ fibTwoPretty 291: GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. 2 292: *** QED
Proofs by Induction (i.e. Recursion)
Next, combining the above operators we specify and prove that
fib is increasing, that is for each natural number i,
fib i <= fib (i+1).
We specify the theorem as a refinement type for fubUp
and use Haskell code to persuade Liquid Haskell that
the theorem holds.
309: {-@ fibUp :: i:Nat -> {fib i <= fib (i+1)} @-} 310: x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | fib x1 <= fib (x1 + 1)}fibUp {v : GHC.Types.Int | v >= 0}i 311: | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 0 312: = {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0 GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 313: *** QED 314: 315: | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 1 316: = {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0 GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2 317: *** QED 318: 319: | otherwise 320: = {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib i 321: GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2) 322: GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib i x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2) ∵ x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | fib x1 <= fib (x1 + 1)}fibUp (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) 323: GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib i x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) ∵ x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | fib x1 <= fib (x1 + 1)}fibUp (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2) 324: GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+1) 325: *** QED
The proof proceeds by induction on i.
The base cases
i == 0andi == 1are represented as Haskell’s case splitting.The inductive hypothesis is represented by recursive calls on smaller inputs.
Finally, the SMT solves arithmetic reasoning to conclude the proof.
Higher Order Theorems
Refinement Reflection can be used to express and verify higher order theorems!
For example, fMono specifies that each locally increasing function is monotonic!
345: {-@ fMono :: f:(Nat -> Int) 346: -> fUp:(z:Nat -> {f z <= f (z+1)}) 347: -> x:Nat 348: -> y:{Nat|x < y} 349: -> {f x <= f y} / [y] 350: @-} 351: x1:({v : GHC.Types.Int | v >= 0} -> GHC.Types.Int) -> (x4:{v : GHC.Types.Int | v >= 0} -> {VV : () | x1 x4 <= x1 (x4 + 1)}) -> x5:{v : GHC.Types.Int | v >= 0} -> x6:{v : GHC.Types.Int | v >= 0 && x5 < v} -> {VV : () | x1 x5 <= x1 x6}fMono {v : GHC.Types.Int | v >= 0} -> GHC.Types.Intf x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | f x1 <= f (x1 + 1)}thm {v : GHC.Types.Int | v >= 0}x {v : GHC.Types.Int | v >= 0 && x < v}y 352: | GHC.Types.Intx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== y 353: = {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f y GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f (GHC.Types.Intx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1) 354: GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int>. {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f x ∵ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | f x1 <= f (x1 + 1)} | v == thm}thm x 355: *** QED 356: 357: | GHC.Types.Intx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 < x2}< y 358: = {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f x 359: GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<. {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f (GHC.Types.Intyx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) ∵ x1:({v : GHC.Types.Int | v >= 0} -> GHC.Types.Int) -> (x4:{v : GHC.Types.Int | v >= 0} -> {VV : () | x1 x4 <= x1 (x4 + 1)}) -> x5:{v : GHC.Types.Int | v >= 0} -> x6:{v : GHC.Types.Int | v >= 0 && x5 < v} -> {VV : () | x1 x5 <= x1 x6}fMono {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | f x1 <= f (x1 + 1)} | v == thm}thm x (GHC.Types.Intyx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) 360: GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<. {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f y ∵ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | f x1 <= f (x1 + 1)} | v == thm}thm (GHC.Types.Intyx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) 361: *** QED
Again, the recursive implementation of fMono depicts the paper and pencil
proof of fMono by induction on the decreasing argument / [y].
Since fib is proven to be locally increasing by fUp, we use fMono
to prove that fib is monotonic.
371: {-@ fibMono :: n:Nat -> m:{Nat | n < m } -> {fib n <= fib m} @-} 372: x1:{v : GHC.Types.Int | v >= 0} -> x2:{v : GHC.Types.Int | v >= 0 && x1 < v} -> {VV : () | fib x1 <= fib x2}fibMono = {v : x1:({v : GHC.Types.Int | v >= 0} -> GHC.Types.Int) -> (x4:{v : GHC.Types.Int | v >= 0} -> {v : () | x1 x4 <= x1 (x4 + 1)}) -> x5:{v : GHC.Types.Int | v >= 0} -> x6:{v : GHC.Types.Int | v >= 0 && x5 < v} -> {v : () | x1 x5 <= x1 x6} | v == RefinementReflection.fMono}fMono {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0 && v == fib x1 && v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | fib x1 <= fib (x1 + 1)} | v == RefinementReflection.fibUp}fibUp
Conclusion
We saw how refinement reflection turns Haskell into a theorem prover by reflecting the code implementing a Haskell function into the function’s output refinement type.
Refinement Types are used to express theorems, Haskell code is used to prove such theorems expressing paper pencil proofs, and Liquid Haskell verifies the validity of the proofs!
Proving fib monotonic is great, but this is Haskell!
Wouldn’t it be nice to prove theorems about inductive data types
and higher order functions? Like fusions and folds?
Or program equivalence on run-time optimizations like map-reduce?
Stay tuned!
Even better, if you happen you be in Nara for ICFP’16, come to my CUFP tutorial for more!