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/theorie... There is work on verifying Data.Set as well: https://github.com/antalsz/hs-to-coq/blob/master/examples/containers/theorie... 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/