Book recommendation: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers [0]. I did read it, but unfortunately I can't say I actually understood it as in to be able to use it day-to-day.

[0] https://www.amazon.ca/Specifying-Systems-Language-Hardware-E...

Backhouse's more playful book, focuses primarily on teaching one how to write and use proofs in the "calculational style" of Dijkstra/Hoare/Lamport/others.

Backhouse's less playful book covers the same topic, but has some more programming examples:

* cyclic code error correction * simple sorting algorithms * real number to integer conversion is used to introduce Galois connections

Again, this isn't a lot in terms of "practical examples". No production level software is built here. If you're looking for that sort of stuff, maybe you want to try out L. Lamport's book: http://www.amazon.com/Specifying-Systems-Language-Hardware-E...

I haven't read that book though.

The article isn't loading for me right now, but I thought I'd mention co-inductive types and how they relate to "interaction".

In Coq, co-inductive types are used to model infinite objects like (never-ending) streams or (non-terminating) program executions.

  Inductive List (A: Set): Set :=
  | Nil: List A
  | Cons : A -> List A -> List A.

  CoInductive Stream (A: Set): Set :=
  | SCons: A -> Stream A -> Stream A.

  Fixpoint len {A: Set} (x: List A): nat :=
    match x with
     | Nil => 0
     | Cons _ y => 1 + len y
    end.

  CoFixpoint ones : Stream nat :=
    SCons nat 1 ones.

If you want to talk about how systems interact with the world, you can use bisimilarity relations to prove "these two systems interact with the world in the same way".

You can also use co-inductive types to embed the temporal logic of actions (TLA) in Coq; TLA is the language Leslie Lamport works with for "Specifying Systems".

* http://www.labri.fr/perso/casteran/RecTutorial.pdf

* http://www.amazon.com/Specifying-Systems-Language-Hardware-E...

* http://en.wikipedia.org/wiki/Bisimulation