Formal verification of containers

[David Feuer]

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 joachim-breitner.de> 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:
> https://hackage.haskell.org/package/containers-verified-0.5.11.0/candidate
> https://github.com/nomeata/containers-verified
>
> I hope that we can extend the covered API somemore in the next weeks :-)
>
>
> Cheers,
> Joachim
>
> --
> Joachim Breitner
>   mail at joachim-breitner.de
>   http://www.joachim-breitner.de/
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180208/f0a1080d/attachment.html>