> [Replying on `scheme-reports' since that's what I was told is the
> preferred way.  I am not affiliated with R7RS in any way.]

"Eli Barzilay <eli at barzilay.org> writes:

[...]

> The problem is demonstrated by Matthew's post, the one that Benjamin
> mentioned, but in a later post he (Benjamin) made the mistake of
> saying:

> | [...] allowing proofs of correctness for Scheme programs to be
> | written much more easily [...]

> and following this line, you reply:

> > Over fifty years ago, John McCarthy brilliantly invented a
> > programming language loosely based on lambda calculus, but designed
> > to be used, not just to be reasoned about [...]

> and all of this is as if immutable pairs are something that fills a
> kind of a theoretical/masochistic need for self punishment in the form
> of correctness proofs.  Something that *real* programmers never have
> to deal with, only "theoreticians of bondage and discipline
> languages".  That couldn't be more *wrong*.  On the side of proofs of
> correctness, there is nothing interesting, really.  The bottom line is
> that this:

>   (define (map f l)
>     (define (loop l)
>       (if (null? l) '() (cons (f (car l)) (loop (cdr l)))))
>     (if (list? l)
>       (loop l)
>       (error "poof!")))

> can be proved as a correct implementation of map *assuming* no changes
> to the list ever occur in the call to `f', or more generally during
> the dynamic extent of the call to `map'.  If you're one of these
> theoretical people, there's not much else to see here.

> The problem is on the side of the *working* programmer -- the one who
> lives in the *real* world.  These people will often make the same
> assumption (and as Matthew points out, they almost always do), so they
> write the above definition and then they're done with it, or rather
> they *think* that they're done.  But the problem starts with the fact
> that Scheme is a language with first-class values -- and `map' happens
> to be a function that uses that: it is a higher order function.  This
> means that you're passing a mutable value to random code -- and this
> random code can now break invariants that your own code (`map', in
> this case) depends on unless you're extra careful.

As I had already mentioned on the scheme-reports-wg1 mailing list, point acknowledged.  So your view is that the main problem with mutable pairs is not about the difficulty of writing proofs of correctness, but about introducing "mutable value[s] to random code," which can now "break invariants that your own code ... depends on."  For a "working programmer" (the group of users whom you feel matter in this case), this is the main concern.

-- Benjamin L. Russell

_______________________________________________
Scheme-reports mailing list
Scheme-reports@scheme-reports.org
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports