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@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@joachim-breitner.de
http://www.joachim-breitner.de/

_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries