Conversation

Jun 12, 2021

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.

Jun 12, 2021

I was going to look at

@RanjitJhala

and

@nikivazou

'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

This Tweet was deleted by the Tweet author. Learn more

Ranjit Jhala

@RanjitJhala

Jun 12, 2021

Very nice! I’ve long wanted to do exactly that ... is there a paper?

Niki Vazou

@nikivazou

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/

Lindsey Kuper

@lindsey

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?

Lindsey Kuper

@lindsey

10:06 AM · Jun 14, 2021Twitter Web App

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.

Replying to

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. 🤔

Replying to

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?)

schmitty/Test_Reflection_Z3_Ints.agda at master · wenkokke/schmitty

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

Replying to

It's not just bindings! There's also reflection, which gets you a lot closer to the look-and-feel of refinement types:

github.com

Agda bindings to SMT-LIB2 compatible solvers. Contribute to wenkokke/schmitty development by creating an account on GitHub.