Synquid: Synthesize Programs from Refinement Types

If you're like me, this immediately lead you to ask, "How are Refinement Types different from Dependent Types?"

In searching for that I found a really good CS stackexchange answer on the subject: https://cs.stackexchange.com/questions/21728/dependent-types...

Which linked to the course materials for a class on Liquid Haskell, which is a refinement types system for Haskell whic lets you prove properties about Haskell programs.

http://ucsd-progsys.github.io/lh-workshop/01-index.html

I found these helpful to think about how Synquid might be doing what it's doing. I really wish I had been at the Strangeloop talk.