(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 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