David,

  2 - After much grovelling over the formal semantics in R5RS, I can say
      that bindings are *not* mutated by anything in that denotational
      specification, locations are. However, denotational specifications
      have the disadvantage that they over-specify the semantics of the
      language in question and strongly suggest a particular
      implementation. Hence R5RS has second-class locations in it's
      formal spec, which I would like to see become first-class. A good
      first-class location SRFI could be a testbed for an RnRS with the
      feature.

There are several other things in a denotational semantics that are what
you would call "second class": environments, stores, etc. The Scheme syntax
has second-class citizens: parameter lists and let/rec/* definitions, which
cannot be the target of macro elaborations. I don't have time to explain
why this is the case and argue should stay so. Scheme is *not* about making
*everything* first-class.

For my dissertation (mid 80s), I developed a semantics, extending the plain
old lambda(value) calculus, that models call/cc, set-struct-field!, etc.
I teach it here, as early as in the freshman course. Here are the two
relevant samples:

------------------------------------------------------------------------
1. Interpreting set!

(define-struct sss (aaa bbb))               (define-struct sss (aaa bbb))

(define some-sss (make-sss 5 'hello)) ==>   (define some-sss (make-sss 5 'hello))

(define a-variable a-value)		    (define a-variable another-value)

... 					    ...

E[(set! a-variable another-value)]          E[(void)]

------------------------------------------------------------------------

2. Interpreting set-struct-field!

(define-struct sss (aaa bbb))               (define-struct sss (aaa bbb))

(define some-sss (make-sss 5 'hello)) ==>   (define some-sss (make-sss 5 'world))

(define a-variable a-value)		    (define a-variable a-value)

... 					    ...

E[(set-sss-bbb! some-sss 'world)]           E[(void)]

------------------------------------------------------------------------

[DrScheme's stepper will explain the behavior of programs with such
transformation rules.]

The rules show what we mean when we say "set! modifies variable-value
bindings" and "set-struct-field! modifes the value but not the binding.
The value before and after the set-struct-field! are eq? and we can even
write this eq? procedure:

(define (eq-sss? a b)
  (let* ([a-aaa (sss-aaa a)]
	 [b-aaa (sss-aaa b)]
	 [_ (set-sss-aaa! a 0)]
	 [_ (set-sss-aaa! b 1)]
	 [result (= (sss-aaa a) (sss-aaa b))]
	 [_ (set-sss-aaa! a a-aaa)]
	 [_ (set-sss-aaa! b b-aaa)])
    result))

-- Matthias