Michael Sperberg-McQueen made this fascinating statement: ... my question [is] focused not on how to prove a transformation correct, but how to specify what correctness is for that transform. I would really like to understand that. What is the difference between “proving a transformation is correct” versus “specifying what correctness is for a transform”? /Roger |