2020-06-15 16:43:47 (GMT)
So there is a draw in the votes (both have 3 votes) and it is time to decide for the paper. I proclaim:
A metaprogramming framework for formal verification
Gabriel Ebner and Sebastian Ullrich and Jared Roesch and Jeremy Avigad and Leonardo de Moura
ICFP 2017
https://leanprover.github.io/papers/tactic.pdf
to be the paper for the next bookclub!
2020-06-15 16:48:59 (GMT)
@Gabriel Ebner it's your paper! Super!
2020-06-25 5:39:33 (GMT)
The link for this afternoon: https://jitsi.mpi-klsb.mpg.de/bookclub_matryoshka
2020-06-25 6:26:57 (GMT)
I'll have to pass due to travel. Have fun!
But if I'm allowed one comment on the paper: Its main weakness, in my opinion, is that it does not honeslty confront the fact that the metaprogramming framework in Lean 3 is extremely slow. I would judge that it's perhaps two orders of magnitude slower than ML programming in Isabelle. As a result, the "super" prover that's mentioned is too slow to be usable, and Gabriel Ebner's attempts at writing a hammer for Lean 3 have stalled. We're all waiting for Lean 4.
2020-06-25 13:43:30 (GMT)