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@joachim-breitner.de http://www.joachim-breitner.de/