Programs are Proofs



Each time you write a program, you are writing a proof!


Proof of what?

Each program proves its type



For each Int there exists an Int:

idInt :: Int -> Int 
idInt x = x


Each program proves its type



For each a there exists an a:

id :: a -> a 
id x = x


Each program proves its type


But, for each Int there exists an a:

idErr :: Int -> a  
idErr x = error "Define me?"


Programs (as proofs) should be well-formed ...

... that is terminating and total.

Each program proves its type


Known as Curry–Howard correspondence

independently developed by Curry (1934) and Howard (1969).


Known as Propositions as Types & Proofs as Programs

by Phil Wadler (2014).

Propositions as Refinement Types


Q: Can you read the following type as a theorem?

f :: x:Int -> y:Int -> {v:() | x + y = y + x}


Q: How would you prove this theorem?


Propositions as Refinement Types


Refined Types are theorems

and

Haskell Functions are proofs.

{-# LANGUAGE TupleSections    #-}
module ProgramsAsProofs where
import Language.Haskell.Liquid.ProofCombinators
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
{-@ onePlusOne :: () -> {v:() | 1 + 1 == 2 } @-}
onePlusOne _ = ()
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Make the theorems pretty!


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


-- import Language.Haskell.Liquid.ProofCombinators
{-@ propOnePlusOne :: () ->  {v: Proof | 1 + 1 == 2} @-}
propOnePlusOne _ = trivial
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Make the theorems even prettier!


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


{-@ propOnePlusOne' :: _ ->  { 1 + 1 == 2 } @-}
propOnePlusOne' _ = trivial *** QED
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Use more SMT knowledge


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


{-@ propPlusAccum :: x:Int -> y:Int -> { x + y == y + x } @-}
propPlusAccum _ _ = trivial *** QED
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Theorems about Haskell functions




Express & Prove Theorems in Haskell ...

... for Haskell functions.

Define (terminating) fib in the logic!

Reflect fib in the logic.

{-@ reflect fib @-}
{-@ fib :: i:Nat -> Nat @-}
fib i | i == 0    = 0
      | i == 1    = 1
      | otherwise = fib (i-1) + fib (i-2)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


(Need to prove fib terminates...)

Structuring Proofs



Using combinators from ProofCombinators!



{-@ fibTwo :: _ -> { fib 2 == 1 } @-}
fibTwo _
  =   fib 2
  ==. fib 1 + fib 0
  *** QED
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Reusing Proofs: The "because" operator



Using combinators from ProofCombinators!



{-@ fibThree :: _ -> { fib 3 == 2 } @-}
fibThree _
  =   fib 3
  ==. fib 2 + fib 1
  ==. 1     + 1      ? fibTwo ()
  ==. 2
  *** QED
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Paper & Pencil style Proofs


fib is increasing

{-@ fibUp :: i:Nat -> {fib i <= fib (i+1)} @-}
fibUp i
  | i == 0
  =   fib 0 <. fib 1
  *** QED
  | i == 1
  =   fib 1 <=. fib 1 + fib 0 <=. fib 2
  *** QED
  | otherwise
  =   fib i
  ==. fib (i-1) + fib (i-2)
  <=. fib i     + fib (i-2) ? fibUp (i-1)
-- 
-- Missing step here !!!
-- 
  *** QED
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Another "Paper & Pencil" Proof


Exercise: Lets fix the proof that fib is monotonic?

{-@ fibMonotonic :: x:Nat -> y:{Nat | x < y } -> {fib x <= fib y}  @-}
fibMonotonic x y
  | y == x + 1
  =   fib x
  <=. fib (x+1) ? fibUp x
  <=. fib y
  *** QED
  | x < y - 1
  =   fib x
  <=. fib (y-1) ? trivial {- Inductive Hypothesis call goes here -}
  <=. fib y     ? fibUp (y-1)
  *** QED
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Exercise: Can you replace trivial to fix the monotonicity proof?

Generalizing monotonicity proof


Exercise: Generalize the implementation of fMono proof below to any increasing function f.

{-@ fMono :: f:(Nat -> Int)
          -> fUp:(z:Nat -> {f z <= f (z+1)})
          -> x:Nat
          -> y:{Nat|x < y}
          -> {f x <= f y} / [y] @-}
fMono f fUp x y
  | y == x + 1
  =   fib x
  <=. fib (x+1) ? fibUp x
  <=. fib y
  *** QED
  | x < y - 1
  =   fib x
  <=. fib (y-1) ? fibMonotonic x (y-1)
  <=. fib y     ? fibUp (y-1)
  *** QED
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Reusing Theorems by Application


fib is monotonic!


{-@ fibMono :: n:Nat -> m:{Nat | n < m }  -> {fib n <= fib m} @-}
fibMono     = fMono fib fibUp
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Recap


Refinements: Types + Predicates
Specification: Refined Input/Output Types
Verification: SMT-based Predicate Subtyping
Measures: Specify Properties of Data
Termination: Well-founded Metrics
Programs as Proofs: Theorem Proving in Haskell


Next: Structural Induction: Program Properties about data types!

Appendix

{-@ LIQUID "--no-warnings"    @-}
{-@ LIQUID "--short-names"    @-}
{-@ LIQUID "--higherorder"     @-}
fib :: Int -> Int
propPlusAccum :: Int -> Int -> Proof
propOnePlusOne :: () -> Proof
onePlusOne :: () -> Proof
fibTwo :: () -> Proof
fibUp :: Int -> Proof
fibThree :: () -> Proof
fMono :: (Int -> Int)
      -> (Int -> Proof)
      -> Int
      -> Int
      -> Proof
fibMono :: Int -> Int -> Proof
fibMonotonic :: Int -> Int -> Proof
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX