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.