I was thinking of adding some kind of 'SMT' universe (or a modality perhaps?) to my language, but I dunno! It doesn't need to be very fancy for this project, I just want to be able to automate away a bunch of stuff to make things easier for users.
Conversation
I was going to look at and 's Refinement Types: A Tutorial and sprite-lang, but I think I'd then need to figure out how to combine it with DTT and semantic typechecking/NbE 🤔
• arxiv.org/abs/2010.07763
• github.com/ranjitjhala/sp
1
5
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
Very nice! I’ve long wanted to do exactly that ... is there a paper?
1
1
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! 🤦♂️
I should probably update the README... 😅
We're still waiting for Agda 2.6.2 to stabilise the library, because until then it still only works with HEAD versions, which is a nightmare to maintain.
1
3
The project description ("Agda bindings to SMT-LIB2 compatible solvers") also undersells it a bit!
1
3
Show replies