Formal verification of containers

[Joachim Breitner]

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/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180131/74a2034e/attachment.sig>