containers-verified: Formally verified drop-in replacement of containers
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-verified in your
.cabal file and earn bragging
rights about using verified data structures in your project. Because the
containers are re-exported, you can still interface with other
libraries that depend on
If you happen to need additional modules or functions, you will have to
depend on both
containers-verified, and use
package-qualified imports to disambiguate.
This package does not re-export any of the
We cannot control which type class instances are re-exported; these therefore
may give you access to unverified code. Also, the
containers 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 real-world 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...)
|Dependencies||containers (==0.6.0.1) [details]|
|Copyright||2018 Joachim Breitner|
|Source repo||head: git clone http://github.com/nomeata/containers-verified|
|Uploaded||by JoachimBreitner at Mon Jun 18 21:18:30 UTC 2018|
|Downloads||152 total (12 in the last 30 days)|
|Rating||(no votes yet) [estimated by rule of succession]|
|Status||Docs available [build log]
Last success reported on 2018-06-18 [all 1 reports]
Hackage Matrix CI
For package maintainers and hackage trustees