Formal verification of containers

[David Feuer]

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.

On Jan 31, 2018 11:18 PM, "Joachim Breitner" <mail at joachim-breitner.de>
wrote:

> Hi containers maintainers,
>
> you might have already read it between the lines, but some people here
> at Penn are currently using hs-to-coq to translate the containers
> library to Coq and verify it. We just reached a milestone by verifying
> a portion of Data.IntSet large enough to instantiate Coq’s
> FSetInterface:
> https://github.com/antalsz/hs-to-coq/blob/master/examples/
> containers/theories/IntSetProofs.v
>
> There is  work on verifying Data.Set as well:
> https://github.com/antalsz/hs-to-coq/blob/master/examples/
> containers/theories/SetProofs.v
>
> Isn’t that exciting?
>
> It raises the question whether there is value in integrating these
> proofs in some way into the development process of containers. One
> could imagine adding a job to travis that translates container’s master
> into Coq and checks if the proofs go through.
>
> On the one hand, that’s of course great, because it’d make containers
> one of the most thoroughly verified pieces of Haskell in use out there.
>
> On the other hand, we’d have to choose the least bad of a bunch of bad
> options when it comes to future contributions (I am listing unfeasible
> options as well):
>
>  - we essentially freeze the code
>  - we’d lose the verification again quickly, once someone makes a non-
>    trivial change to the code
>  - we’d have to restrict contributions to those who are able to update
>    the proofs
>  - 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
>  - (maybe a bit far fetched, but who knows)
>    we get funding to pay someone to keep the proofs in sync, without
>    slowing down other contributions
>
> I honestly don’t know which of these are the most viable, or if none of
> them make any sense and we should not hook up the verification with
> container’s development.
>
> What do you think?
>
> Cheers,
> Joachim
>
> --
> Joachim Breitner
>   mail at joachim-breitner.de
>   http://www.joachim-breitner.de/
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180201/b421406b/attachment.html>