<div dir="auto">I don't think we should limit containers development like that. I do imagine it would be valuable to have a separate package, perhaps called verified-containers, that tries to stay a few weeks or months behind containers.</div><div class="gmail_extra"><br><div class="gmail_quote">On Jan 31, 2018 11:18 PM, "Joachim Breitner" <<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi containers maintainers,<br>
<br>
you might have already read it between the lines, but some people here<br>
at Penn are currently using hs-to-coq to translate the containers<br>
library to Coq and verify it. We just reached a milestone by verifying<br>
a portion of Data.IntSet large enough to instantiate Coq’s<br>
FSetInterface:<br>
<a href="https://github.com/antalsz/hs-to-coq/blob/master/examples/containers/theories/IntSetProofs.v" rel="noreferrer" target="_blank">https://github.com/antalsz/hs-<wbr>to-coq/blob/master/examples/<wbr>containers/theories/<wbr>IntSetProofs.v</a><br>
<br>
There is work on verifying Data.Set as well:<br>
<a href="https://github.com/antalsz/hs-to-coq/blob/master/examples/containers/theories/SetProofs.v" rel="noreferrer" target="_blank">https://github.com/antalsz/hs-<wbr>to-coq/blob/master/examples/<wbr>containers/theories/SetProofs.<wbr>v</a><br>
<br>
Isn’t that exciting?<br>
<br>
It raises the question whether there is value in integrating these<br>
proofs in some way into the development process of containers. One<br>
could imagine adding a job to travis that translates container’s master<br>
into Coq and checks if the proofs go through.<br>
<br>
On the one hand, that’s of course great, because it’d make containers<br>
one of the most thoroughly verified pieces of Haskell in use out there.<br>
<br>
On the other hand, we’d have to choose the least bad of a bunch of bad<br>
options when it comes to future contributions (I am listing unfeasible<br>
options as well):<br>
<br>
- we essentially freeze the code<br>
- we’d lose the verification again quickly, once someone makes a non-<br>
trivial change to the code<br>
- we’d have to restrict contributions to those who are able to update<br>
the proofs<br>
- we’d still welcome contributions that break the proofs, but let them<br>
<br>
sit in pull requests until someone updates the proofs on the PR and<br>
then merge<br>
- (maybe a bit far fetched, but who knows)<br>
we get funding to pay someone to keep the proofs in sync, without<br>
slowing down other contributions<br>
<br>
I honestly don’t know which of these are the most viable, or if none of<br>
them make any sense and we should not hook up the verification with<br>
container’s development.<br>
<br>
What do you think?<br>
<br>
Cheers,<br>
Joachim<br>
<br>
--<br>
Joachim Breitner<br>
<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a><br>
<a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.<wbr>de/</a><br>
<br>______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
<br></blockquote></div></div>