⚠️ This post is archived from my phlog in Gopherspace. Please read my post on the Gopher Protocol to get started!
This article helps you get started with LiquidHaskell, which I found confusing.
I use LiquidHaskell’s refinement types which allows you to…
formal verification is like property testing, but instead of n statistical samples providing evidence it’s a solver providing proof
ghcid -c “stack ghci”
put this in header of file to doctest:
{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
the example project has stack examples fore ach version. it’s very tricky to add the right dependencies to stack so use the examples from the repository–there’s a stack file per ghc version.
https://github.com/ucsd-progsys/lh-plugin-demo/tree/main
https://github.com/ndmitchell/ghcid
https://ucsd-progsys.github.io/liquidhaskell/install/
i’m actually using regular haskell plugin
Original content in gopherspace: gopher://gopher.someodd.zip:70/0/phlog/liquidhaskell-verification-stack.txt