On Mon, 26 Jun 2006, David Feuer wrote:

> Should marks and substitutions be considered part of the
> specification, or an implementation technique?  I would suggest that
> the SRFI author try to find a way to specify the macro system
> precisely without going into details of how the expander is
> implemented.

I like the operational semantics in the SRFI, since it may be less ambiguous
than the alternative declarative approach.

As corrobrating evidence, I can mention the syntax-case implementation in
SRFI-72.  That implementation satisfies declarative descriptions of
hygiene.  However, the implementation technique is based on an "implicitized"
version of explicit renaming, not marking/substitution.  There are some highly
obscure corner cases where it behaves differently from the marking algorithm,
while still satisfying hygiene.  I have to recheck, but I think these
ambiguities should be resolved by specifying the algorithm as is
done here (though perhaps a little more detail might be required).

Regards
Andre