https://www.youtube.com/watch?v=Q-3tcbUyF34 is a wonderful talk showing how to generate whole programs from just a liquid haskell type definition with Synquid.