Formal verification of containers

David Feuer david.feuer at
Thu Feb 1 05:02:14 UTC 2018

I don't think we should limit containers development like that. I do
imagine it would be valuable to have a separate package, perhaps called
verified-containers, that tries to stay a few weeks or months behind

On Jan 31, 2018 11:18 PM, "Joachim Breitner" <mail at>

> Hi containers maintainers,
> you might have already read it between the lines, but some people here
> at Penn are currently using hs-to-coq to translate the containers
> library to Coq and verify it. We just reached a milestone by verifying
> a portion of Data.IntSet large enough to instantiate Coq’s
> FSetInterface:
> containers/theories/IntSetProofs.v
> There is  work on verifying Data.Set as well:
> containers/theories/SetProofs.v
> Isn’t that exciting?
> It raises the question whether there is value in integrating these
> proofs in some way into the development process of containers. One
> could imagine adding a job to travis that translates container’s master
> into Coq and checks if the proofs go through.
> On the one hand, that’s of course great, because it’d make containers
> one of the most thoroughly verified pieces of Haskell in use out there.
> On the other hand, we’d have to choose the least bad of a bunch of bad
> options when it comes to future contributions (I am listing unfeasible
> options as well):
>  - we essentially freeze the code
>  - we’d lose the verification again quickly, once someone makes a non-
>    trivial change to the code
>  - we’d have to restrict contributions to those who are able to update
>    the proofs
>  - we’d still welcome contributions that break the proofs, but let them
>    sit in pull requests until someone updates the proofs on the PR and
>    then merge
>  - (maybe a bit far fetched, but who knows)
>    we get funding to pay someone to keep the proofs in sync, without
>    slowing down other contributions
> I honestly don’t know which of these are the most viable, or if none of
> them make any sense and we should not hook up the verification with
> container’s development.
> What do you think?
> 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