Formal verification of containers

[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.

On Feb 1, 2018 10:17 PM, "Gershom B" <gershomb at gmail.com> wrote:

> In the initial message, Joachim suggested “One could imagine adding a job
> to travis that translates container’s master into Coq and checks if the
> proofs go through.”
>
> It would seem to me that an ideal situation would be if there were
> “proof-tests” similar to doctests. Essentially, portions of code that have
> corresponding Coq proofs about them have an annotation that indicates the
> proofs, and indicates to the automated job that they are to be tested
> against those proofs. When changes are made that do not have corresponding
> updates to the proofs, then the corresponding annotations would need to be
> commented-out (or perhaps, replaced with some other annotation that
> explicitly indicates a skipped or missing proof).
>
> This would let the proper containers core be verified, with
> mechanically-checked annotations indicating where the verification hasd and
> has not been performaed. Some sort of re-exported subset of only the
> verified stuff could then be automatically extracted from this setup for
> users that wanted to restrict themselves to only this subset.
>
> —g
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180201/553ebe4b/attachment.html>