[racket-dev] syntax-property guards? (was: Re: The Stepper strikes again)

On Sat, Aug 13, 2011 at 1:26 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> On Aug 13, 2011, at 12:58 PM, Sam Tobin-Hochstadt wrote:
>
>> On Sat, Aug 13, 2011 at 12:51 PM, Eli Barzilay <eli at barzilay.org> wrote:
>>> 10 minutes ago, Sam Tobin-Hochstadt wrote:
>>>> `match' also currently adds a syntax property to help the Typed
>>>> Racket type checker understand the expansion.  Like 'disappeared-use
>>>> for Check Syntax, this property is in theory semantically
>>>> independent of Typed Racket, but only used there.
>>>
>>> No, when your property is called `typechecker:called-in-tail-position'
>>> it is not independent of a "typecheker".  It will be, if it gets a
>>> generic name, and gets documented which turns it from a backdoor for a
>>> backward dependency to a known API.
>>
>> The *semantic* independence of the property and the typechecker
>> implementation is not determined either by the name of the property or
>> the documentation.
>
>
> There are two levels of semantics here:
>  -- operational semantics of your module, which makes you correct
>  -- 'in spirit' semantics, which makes Eli correct.
>
> I will say that even though I cannot define 'in spirit' formally,
> I am with Eli here.

How about instead of "in spirit", we focus on program logic.  There is
no semantic dependence on the typechecker -- Racket can tell what the
program does without it.  However, programmers cannot read that code
and know what it is for and whether it is correct without reference to
the typechecker.  That's a meaningful dependency.  It makes
maintaining that line of code 100% dependent on the typechecker.

--Carl