Past Meetup

Joachim Breitner - Who needs theorem provers when we have compilers?

This Meetup is past

32 people went

Details

This is an out-of-schedule meetup, as Joachim Breitner a world-class Haskell researcher (http://www.joachim-breitner.de/publications) is visiting Zurich and offered to give a talk with the following abstract:

After decades of work on functional programming and on interactive theorem proving, a Haskell programmer who wants to include simple equational proofs in his programs, e.g. that some Monad laws hold, is still most likely to simply do the derivation as comments in the file, as all the advanced powerful proving tools are inconvenient.

But one powerful tool capable of doing (some of) these proofs is hidden in plain sight: GHC, the Haskell compiler! Its optimization machinery, in particular the simplifier, can prove many simple equations all by himself, simply by compiling both sides and noting that the result is the same. Furthermore, and crucially to make this approach applicable to more complicated equations, the compiler can be instructed to do almost arbitrary symbolic term rewritings by using Rewrite Rules.

In this informal ad-hoc talk I will show a small GHC plugin that I can use to prove the monad laws for a non-trivial functor. I am looking forward to a discussion of the merits, limits and capabilities of this approach