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
Like, if you make a type using the embedded refinement thingy it would automagically call the solver to construct proof terms for you as-needed. Not sure if that's possible though (sounds a bit tricky?)
1
Might also be interesting include Why3 in these comparisons too. It lets you use a range of different proof tools (solvers, theorem provers, etc) discharge verification conditions: why3.lri.fr