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"
(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@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries