[r6rs-discuss] [Formal] Equivalence predicate version of memp

From: Carl Eastlund <cce>
Date: Thu Sep 28 15:44:34 2006

On 9/28/06, Andre van Tonder <andre_at_het.brown.edu> wrote:
> William Clinger wrote:
>
> > There are at least four differences between forall and
> > exists in the draft R6RS and every and any in SRFI-1:
> >
[...]
>
> This kind of ambiguity could be easily fixed by specifying these
> procedures via exhibiting a correct reference implementation
> with (or even instead of much of) the prose description.
> Since the length of the simplest correct implementation is
> mostly very short, the increase in spec length, if any,
> would likely be modest.
>
> There is in fact another, more compelling, reason for doing
> just this. The current specification of various of the list
> procedures is ambiguous in the presence of call/cc. This
> is the subject of a formal comment I just submitted.
>
> Specifying these procedures via implementation would fix
> these call/cc ambiguities, ambiguities in the prose, and perhaps
> some other possibly unknown ambiguities (exceptions come to mind).
> Any concomitant increase in spec length would therefore be well
> worth it.

There would still need to be prose explaining how an implementation
can differ from the code in the specification. Otherwise,
implementations would have to use the specification verbatim to match
its behavior in terms of space and time complexity, order of
operations, handling exceptional cases, and so on. It's just as easy
to overspecify with code as it is to underspecify with prose.

I have no personal objection to a specification written either way,
but both ways require care and precision.

-- 
Carl Eastlund
Received on Thu Sep 28 2006 - 15:44:19 UTC

This archive was generated by hypermail 2.3.0 : Wed Oct 23 2024 - 09:15:01 UTC