Untangle Your Spaghetti with Liquid Haskell
Please log in to watch this conference skillscast.
Liquid Haskell (LH) is a tool regarded to verify programs. In this talk, however, we will look at using it as a tool to understand what a program is doing via specifications. We will look at a gnarly function (Data.List.permutations) from the base library and show how its meaning can be unraveled by writing down specifications for each piece of the implementation, while having LH prove that the pieces really do what the specifications say!
This talk targets universal engineering needs like explaining how a function works, verifying that the explanation is accurate, and ensuring that it stays up-to-date. The lack of documentation of the chosen function had an observable impact in the community this year [1]. LH is attractive to solve these problems because, unlike other approaches, it doesn't require extending the Haskell language, and it reuses the effort that goes into developing dedicated tools to reason about logic like SMT solvers.
YOU MAY ALSO LIKE:
- Untangle Your Spaghetti with Liquid Haskell (SkillsCast recorded in December 2022)
- Scala Days 2023 (Online Conference on 1st - 30th December 2023)
- Teaching Haskell...To High Schoolers! (SkillsCast recorded in December 2022)
- Teaching Haskell...To High Schoolers! (SkillsCast recorded in December 2022)
Thank you to our sponsors and partners
Platinum
Gold
Silver
Bronze
Partners
Untangle Your Spaghetti with Liquid Haskell
Facundo Domínguez
Facundo Domínguez is a software engineer at Tweag. He has been using Haskell in industry during the last two decades, and he is a long-time contributor to Haskell libraries and GHC. Of late, he has been contributing to Liquid Haskell to make it easier and faster to use until it takes over the world.