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@joachim-breitner.de
http://www.joachim-breitner.de/
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries