Formal verification of containers

[David Feuer]

containers-verified should only export the verified part, for sure. I think
it should mostly re-export, but if it needs to use a different version of a
function (perhaps temporarily) then it can do so. For example, if
containers makes a function faster at the expense of some complication,
then containers-verified may want to stick with the old version until the
new one can be verified (or someone can come up with a simpler fast one).

On Feb 1, 2018 9:15 AM, "Joachim Breitner" <mail at joachim-breitner.de> wrote:

> 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/
>
> _______________________________________________
> 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/20180201/8d833f79/attachment.html>