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