u/meiersiin r/haskell • Recommends
2017 03 09 - Joachim Breitner - Why use theorem provers when we have compilers
0:00 / 0:00
2017 03 09 - Joachim Breitner - Why use theorem provers when we have compilers
Simon Meier
244 subscribers • 6 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Joachim Breitner
- Linked in the descriptionnomeata/ghc-proofs
Advanced. Deep dive for people who know the field.
1.4K views9 years ago1 recommendation
Programming languagesSystems programmingCompilers and interpretersComputation and complexityFormal methods and verification
Joachim Breitner explains how to use GHC's compiler optimizations to prove program equivalences instead of relying on external theorem provers.
HaskellerZ talk from this march. Related Github repository: github.com/nomeata/ghc-proofs. Related blogpost: joachim-breitner.de/blog/717-Why_prove_programs_equivalent_w…Why it's here
1 person recommends thisWhat people say. Recommended as an interesting look at using GHC's optimization engine for formal proofs.
u/nomeatain r/haskell • Mentions
On “Definitional lawfulness: proof by inspection testing”
Very nice! Curiously, the inspiration for `inspection-testing` came from `ghc-proofs`, which is a plug-in to do the kind proof that Li-yao is doing here. See https://github.com/nomeata/ghc-proofs and my talk “Who needs theorem provers when we have compilers?”.
Back then I concluded that these proofs are cute, but not very useful, but that the same idea, rebranded as inspection testing might actually be useful.