Formal verification of containers

[Joachim Breitner]

Hi,

Am Donnerstag, den 01.02.2018, 22:25 -0500 schrieb David Feuer:
> Oh, I'm perfectly fine with *checking* everything. But to give the
> users who want verification a consistent API, the verified package
> will probably have to include old or modified versions of some
> functions or even modules.

at the moment, we don’t have to modify containers. To be precise, we
don’t have to modify it’s source. The translation to Coq does a few
modification, such as highestBitMask, which uses raw pointers, which we
cannot translate.

I don’t expect that this will change. But it is true that if containers
changes their code in a way that breaks the proofs (which is not every
change – we work on what GHC sees after parsing and renaming, so a fair
amount of changes might not even affect the proofs), then containers-
verified would have to stick with the old version.

A viable approach might be a containers-verified package that depends
on a precise version of containers and re-exports the verified subset
of containers. It might lag a few versions behind, but for something
stable like containers, that might still be useful for people who want
bragging rights about using verified code.

Practically, the verification has not uncovered any bugs yet (unless
one counts the incomplete implementation of `valid` for IntSet, but
that only affects the test suite), so users will not gain too much…

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/20180201/8480d4d3/attachment.sig>