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