homepage: https://github.com/nomeata/containers-verified
changelog-type: markdown
hash: 18dbe519685935ef9c833a666278e48a1e4f77bb58676dc719eaf5e84f95d348
test-bench-deps: {}
maintainer: mail@joachim-breitner.de
synopsis: Formally verified drop-in replacement of containers
changelog: ! '# Revision history for containers-verified


  ## 0.5.11.0 -- 2018-03-15


  * First version.

'
basic-deps:
  containers: ==0.5.11.0
all-versions:
- '0.5.11.0'
author: Joachim Breitner
latest: '0.5.11.0'
description-type: haddock
description: ! 'In the context of the <https://deepspec.org/main DeepSpec project>,
  parts of the

  <http://hackage.haskell.org/package/containers containers> library were

  formally verified using <https://github.com/antalsz/hs-to-coq 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

  <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#package-qualified-imports
  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...)'
license-name: MIT

Update from Hackage at 2018-03-16T00:56:26Z
Update from Hackage at 2018-03-16T00:56:26Z
