Formal verification of containers

[David Feuer]

It sounds nice, but keeping the verified version up to date requires a
steady supply of very highly skilled labor. I personally don't think it
reasonable to even consider making containers itself the verified version
unless the verifiers are able to

1. Stay fairly up to date for a good while (say five or six years, after
the current researchers have gotten their degrees/professorships), AND
2. At the end of that period, explain their plan for continuing the effort.

On Feb 1, 2018 9:50 PM, "Tom Murphy" <amindfv at gmail.com> wrote:

> (My 2 cents, not as a containers developer)
>
> First of all, bravo! This is great news.
>
> On Wed, Jan 31, 2018 at 11:17 PM, Joachim Breitner <
> mail at joachim-breitner.de> wrote:
>
>>
>>  - we’d still welcome contributions that break the proofs, but let them
>>    sit in pull requests until someone updates the proofs on the PR and
>>    then merge
>>
>
> If we imagine, as David does, that updating proofs will take a couple of
> weeks (or months), I'd imagine an advantage of this option is that:
>   - The percent of containers users who only use features older than weeks
> or months from bleeding edge: 95+%
>   - The percent of end-users who will realistically switch their code from
> containers to containers-verified: certainly less than 20%
>
> If we can seamlessly switch the vast majority of users to this new
> verified code, and be able to say that a ubiquitous component of Haskell
> development is formally verified, I'd say that's a huge accomplishment.
>
> An alternative proposal would be to have a "containers-unverified"
> *upstream* instead of a "containers-verified" downstream. This would also
> neatly sidestep the problem of if "containers-verified" should export
> unverified code: it's just "containers" as usual, just with some extra
> verification.
>
> Tom
>
>
> _______________________________________________
> 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/288f4aeb/attachment-0001.html>