containers-verified: Formally verified drop-in replacement of containers

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.


In the context of the DeepSpec project, parts of the containers library were formally verified using hs-to-coq and the interactive theorem prover Coq.

This package depends on precisely the verified version of containers and re-exports the verified parts of the API, with module name and function name unchanged.

If you happen to use only the verified subset of the API, then you can simply change containers to containers-verified in your .cabal file and earn bragging rights about using verified data structures in your project. Because the types from containers are re-exported, you can still interface with other libraries that depend on containers directly.

If you happen to need additional modules or functions, you will have to depend on both containers and containers-verified, and use package-qualified imports to disambiguate.

This package does not re-export any of the ….Internals modules.

We cannot control which type class instances are re-exported; these therefore may give you access to unverified code. Also, the conatiners code contains some CPP directives; these can enable different code on your machine than the code that we verified (e.g. different bit-widths).

To learn more about what exactly has been verified, and how wide the formalization gap is, see the paper “Ready, Set, Verify! Applying hs-to-coq to non-trivial Haskell code” by Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley and Stephanie Weirich.

The long-term maintenance plan for this package is not fleshed out yet, and certainly depends on user-demand. Let us know your needs! (And your technical or financial abilities to contribute...)


Dependenciescontainers (== [details]
Copyright2018 Joachim Breitner
AuthorJoachim Breitner
Home page
Source repositoryhead: git clone
UploadedFri Mar 16 00:46:09 UTC 2018 by JoachimBreitner




Maintainers' corner

For package maintainers and hackage trustees