Formal verification of containers

[Joachim Breitner]

Hi,

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!
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?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
contributors.

Cheers,
Joachim


-- 
Joachim “nomeata” Breitner
  mail at joachim-breitner.de
  https://www.joachim-breitner.de/
-------------- 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: <http://mail.haskell.org/pipermail/libraries/attachments/20180201/07fa38bd/attachment.sig>