The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

The first thing which pops to my mind is Charguéraud's work on so-called characteristic formulæ of ml programs. But I don't think it will fit your bill of understandability.

The state monad may be a good idea (though you'll probably have to talk about exceptions too). It's not different than explicit state passing in that it is just another word for explicit state-passing. But people have been using dependent flavour of the state monad to get some Hoare-style logic. On that subject there is Wouter Swierstra's The Hoare State Monad, and the more ambitious Ynot project headed by Greg Morrisett.

Take you pick.

On 7 August 2014 19:27, Dmitry Grebeniuk <gdsfh1 AT gmail.com> wrote:

Hello.

  I've asked this question in #coq irc, but with no practical success,
so I'm asking here.
  I want to prove an algorithm that involves mutable data structures
(namely, direct acyclic graph with mutable data associated with
vertices), some global mutable state, and recursion used to walk the
graph and modify vertex values.
  I can't use immutable data structures in my code: it would be
inconvenient for people who use my code, and it would be not
performance-wise.
  Also I don't need code extraction: manual porting of Coq code to
OCaml will be more or less straightforward.  I don't want to use Why,
because I want to understand every bit of my representation and
proofs.  (think it's a pedagogical purpose of this task.)
  A toy example of code I want to reason about:
https://gist.github.com/gdsfh/b5fc400f3e931e0194ad
  Here I want to prove that after calling "setmax somenode" all nodes
below "somenode" have "fld = max(n.fld)", where n are direct and
indirect children; and fld of leaf nodes is left intact.
  "State" monad is not very useful, since I have to prove things like
"eval (a := 1; a := 2) ==(after it..)==> eval(a) == 2", and state
monad won't ease proofs compared to explicit state passing.  (am I
wrong?)
  Which keywords, papers or pointers can you suggest?