Formal verification of containers

David Feuer david.feuer at
Thu Feb 8 23:50:28 UTC 2018

Interesting! I look forward to seeing more. One possible twist would be to
wrap the re-exported types in newtype wrappers to hide the unverified
instances, perhaps in a separate Wrapped module. But that might be more
trouble than it's worth. When you get to it, there are some hard-coded size
limits in Data.Map.alterF for word sizes below 61 bits that I would *love*
to see checked formally; I trust those less than pretty much anything else
in the package, and testing them is hard.

On Feb 8, 2018 6:21 PM, "Joachim Breitner" <mail at> wrote:

> Hi,
> Am Donnerstag, den 01.02.2018, 23:01 -0500 schrieb Joachim Breitner:
> > A viable approach might be a containers-verified package that depends
> > on a precise version of containers and re-exports the verified subset
> > of containers. It might lag a few versions behind, but for something
> > stable like containers, that might still be useful for people who want
> > bragging rights about using verified code.
> here is how this could look like:
> I hope that we can extend the covered API somemore in the next weeks :-)
> Cheers,
> Joachim
> --
> Joachim Breitner
>   mail at
> _______________________________________________
> Libraries mailing list
> Libraries at
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Libraries mailing list