Formal verification of containers

Joachim Breitner mail at
Thu Feb 1 16:09:46 UTC 2018


Am Donnerstag, den 01.02.2018, 15:35 +0100 schrieb Henning Thielemann:
> On Thu, 1 Feb 2018, Joachim Breitner wrote:
> > I guess there are a view variants:
> > 
> > Should containers-verified export only the verified subset of the API,
> > or all of it? The former is more honest, the latter easier to switch to
> > for users.
> ... then the question: Should containers-verified export Data.Map or 
> Data.Map.Verified? If it exports Data.Map but not all other modules of 
> 'containers', then there would be no way to access all modules of 
> 'containers'. So maybe containers-verified should export 
> Data.Map.Verified.

Valid point. I guess we should just verify all of it :-)

There is the option of using package-qualified imports!

The question would be whether we put a little burden on those users who
need to mix-and-match, or on those who would be happy with the portion
of the API provided by containers-verified.

Not renaming also makes it easier to merge changes from containers, but
 not by a lot.

> But then you can as well add Data.Map.Verified to 
> 'containers'.

Not really, the main reason to split it off is to not impose the burden
of the verification infrastructure on container’s maintainers and/or


Joachim “nomeata” Breitner
  mail at
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <>

More information about the Libraries mailing list