Very nice! I’ve long wanted to do exactly that ... is there a paper?
This Tweet was deleted by the Tweet author. Learn more
Conversation
Lean4 is definitely in this direction, with SMT automatic on top and a small intentional kernel at the back. I am not aware of a paper, but their tutorial is very good: leanprover.github.io/lean4/doc/
1
1
5
I really want to better understand this design space (the "integrated automatic/interactive proving" space, although I don't care for that terminology much). How do Lean and F* compare to LH, for instance?
1
3
I think there's a whole survey paper to write. I'd also consider various tools that let you talk to SMT solvers from Coq or Agda to be in scope.
1
4
I saw that made this library for Agda: github.com/wenkokke/schmi - I think it might just be bindings, but it's still pretty cool! I wonder if you could somehow use this to embed LH-style refinements into Agda. 🤔
3
1
3
It's not just bindings! There's also reflection, which gets you a lot closer to the look-and-feel of refinement types:
2
5
OOOHH! NICE! 🤩
I think I might have clicked on exactly the wrong test when trying to figure out if there was more than the bindings. Sorry for misrepresenting your work! 🤦♂️
1
3
The project description ("Agda bindings to SMT-LIB2 compatible solvers") also undersells it a bit!
1
3
Strongly agree, haha! It's far more than that! 😊