My dream is to bring formal verification into everyday programming and I pursuit my dream under a post-doc position at University of Maryland.
Haskell is my favorite programming language because I find programming with functions the natural way to go and also I never figured out how to prevent null pointer, runtime exceptions.
At UC San Diego, we developed Liquid Haskell that extends Haskell types with logic with a goal to catch more exceptions before runtime.
Even though Liquid Haskell uses sophisticated verification techniques, they are hidden behind its user-friendly interface.
In my talk, I aim to persuade you that Liquid Haskell is indeed both usable and useful.
We present Refinement Reflection, a method to extend legacy languages---with highly tuned libraries, compilers, and run-times---into theorem provers.
The key idea is to reflect the code implementing a user-defined function into the function's (output) refinement type.
As a consequence, at uses of the function, the function definition is unfolded into the refinement logic in a precise and predictable manner.
We have implemented our approach in Liquid Haskell thereby retrofitting theorem proving into Haskell.
We show how to use reflection to verify arithmetic properties of common recursive functions as well as program equivalence of computations that use Haskell’s highly tuned parallel runtime environment.