Embed Notice

... #LiquidHaskell (restriction types, SMT solver) and the Isabelle proof assistant.

For example, look at the kind of assurances we can make about data at the type-level. This means the SMT solver can assure that certain logical constraints on types are provably true.

My code to verify a file ranking algo I made:

https://github.com/someodd/bore/blob/master/src/Bore/SpacecookieClone/Search/Verified.hs