[Axiom-developer] Embedding Axiom (Hickey and fold/unfold)

[Tim Daly]

There is an excellent talk by Rich Hickey about modelling time, 
identity, values,
perception, state, memory, etc.

http://www.infoq.com/presentations/Are-We-There-Yet-Rich-Hickey


I think it adds quite a bit to the Embedded Axiom idea set. If we kept 
immutable
intermediate states we could easily run a  computation forward and backward.

We can combine that immutable idea with the fold/unfold idea from functional
programming. The idea is that you can do program proofs by expanding
a definition by unfolding and contracting a definition by folding.

http://www.cs.nott.ac.uk/~gmh/bib.html#semantics

The analog of this idea, at least as I perceive it, is the same as doing
operations on both sides of an equation. If we want to prove things
about a computation we could work backward from the result by
unfolding to some intermediate point, and forward from the input by
unfolding to the same intermediate point. If they match then there is
a fold/unfold path between them.

Tim