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
{-@ onePlusOne :: () -> {v:() | 1 + 1 == 2 } @-} onePlusOne _ = ()

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

Make the theorems even prettier!


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


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

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

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)


(Need to prove fib terminates...)

Structuring Proofs



Using combinators from ProofCombinators!



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

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

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

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

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

Reusing Theorems by Application


fib is monotonic!


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

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