Liquid Haskell is a verifier of Haskell programs that hooks as a plugin into the GHC compiler. Like other projects with tight integration with the GHC API, it is a struggle to keep it up-to-date when new releases of GHC come out. Liquid Haskell, with near 60000 lines of code, requires much programming and debugging during upgrades.

If only Liquid Haskell and GHC were the same project then Liquid Haskell would not need to catch up. But does this solve the problem? No! Because then the GHC developers would need to deal with the breakages in yet another complex piece of software.

Another factor in the analysis is the luring assumption that merging the projects would provide a better experience to Liquid Haskellers since Liquid Haskell logic could be integrated into the Haskell language; an assumption that we will examine closely.

This talk goes over the challenges of maintaining a client of the GHC API, and the trade-offs when deciding how much to integrate with Haskell and GHC.

Facundo is a software engineer supporting development and research projects at Tweag. Prior to joining Tweag, he worked in academia and in industry, on a varied assortment of domains, with an overarching interest in programming languages.

Currently, Facundo is leading the collaboration of Tweag with the authors of Liquid Haskell to integrate SMT solvers into the day-to-day practices of the software industry. He is also the maintainer of inline-java and sparkle, and has made multiple contributions to GHC, rules_haskell, and the Haskell libraries. His everyday activities include elaborating project proposals, development, software verification, and mentoring.

He received a MSc in Computer Science at Universidad de la República in Montevideo, researching program transformation techniques. Since then he worked in software projects for education, entertainment, finance, scientific computation, and government.