Formal verification of containers

[Joachim Breitner]

Hi

Am Donnerstag, den 01.02.2018, 11:42 +0100 schrieb Henning Thielemann:
> On Thu, 1 Feb 2018, David Feuer wrote:
> 
> > 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 
> > containers.
> 
> I am happy to change all my dependencies from 'containers' to 
> 'containers-verified' (for easier association in a lexicographically 
> ordered list).

that is an interesting idea, and a nicely generalizable pattern,
David. 

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.

Should it
 a) simply depend on a particular version of containers, and re-export 
    the functions, or
 b) be a real code copy, or
 c) be a code copy with the exception of the data types, so that you
    can interoperate with the existing containers library?

b (maybe even with hiding the ….Internals module) prevents users from
creating non-well-formed trees, but it would prevent you from using
containers-verified in a library that exports the types as part of its
API. Maybe one could add “toVerified” and “fromVerified” functions that
convert between the two, with run-time checks?


Cheers,
Joachim



-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://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/3ae6aec2/attachment.sig>