Formal verification of containers

David Feuer david.feuer at
Fri Feb 2 03:03:09 UTC 2018

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> 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> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Libraries mailing list