SAT solvers are starting to be used as tooling for functional languages - Liquid Haskell uses one for refinement types[1], and Djinn uses one for suggesting fun

SAT solvers are starting to be used as tooling for functional languages - Liquid Haskell uses one for refinement types[1], and Djinn uses one for suggesting functions given a type[2]. Similarly to Djinn, Edwin Brady gave a presentation on using an SMT solver to do live code suggestions/implementation inference in the successor to Idris[3]. [1] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/ [2] http://lambda-the-ultimate.org/node/1178 http://lambda-the-ultimate.org/node/1178 [3] https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU