Re: Bindings and guard-based auditing

On 25 May 2010 17:41, Kevin Reid <kpreid-M/[email protected]> wrote:
> On May 25, 2010, at 11:03, Thomas Leonard wrote:
>
>> For the slots-only case, I'm imagining that there's some method on
>> Slot
>> to get details for an auditor (getAuditionInfo or some-such). This is
>> only called for known slot types (FinalSlot, VarSlot, etc). For other
>> slot types, we pass no information to auditors.
>>
>> (yes, this makes some slot types special, but as I understand it the
>> bindings proposal makes certain binding types special)
>
> What do you mean by "binding types"?

I'm assuming I can't do:

def &&x := makeMyBinding(...)

> Note that 'CoercedSlot' does not mean 'a (container for a) slot which
> has been coerced'; it means 'a slot whose value *has been* coerced';
> it is basically GuardedSlot without the mutability.

I'm still confused, then. How can the value have been coerced, unless
it's a FinalSlot. Other slots change their value over time.

>> But in:
>>
>>  def &x := makeSlot(...)
>>
>> the information given up to an auditor would depend on makeSlot
>> (whereas
>> with bindings no information is given up), and in
>
> Is 'makeSlot' here a builtin or some user-defined function?

User-defined (but returning a slot wrapped in a built-in slot type if
it wants it to be auditable immediately).

>> For wacky slots:
>>
>>  def &&wacky := makeCoercedSlot(WackySlot, makeWackySlot(value))
>>
>> becomes
>>
>>  def &wacky :CoercedSlot[WackySlot] := makeWackySlot(value)
>>
>> where CoercedSlot is a trusted slot type which simply proxies to the
>> underlying slot, coerced by the guard. It gives up the guard
>> (WackySlot)
>> to the auditor, which can process it as it pleases. makeWackySlot
>> could
>> do the coercion itself if desired.
>
> I don't see what this CoercedSlot (please don't call it that, BTW;
> this is different from what CS in the GBA proposal does) adds;
> wouldn't it be sufficient to have the following?
>
>    def &wacky :WackySlot := makeWackySlot(value)

Yes, or even:

  def &wacky := makeWackySlot(value)

> In current (pre- or post-GBA) E semantics, this coerces the rvalue by
> WackySlot before storing it as the slot for 'wacky'.
>
> ...Oh, I see. We put the slot in a wrapper which is known to give
> reliable information to the auditors; in this particular case 'the
> behavior of this slot, as a slot, is that enforced by WackySlot'.

Yes.

>> The main difference is that bindings add new syntax (&&x and "def ...
>> as").
>
> As a historical note:
>
> The && syntax was added primarily so that sugar expansions which
> rebind values (such as &&, ||, and 'extends') can preserve binding
> guards.
>
> The 'as' syntax was added so that the bindings of object definitions
> could have information for auditors, without having to write e.g. def
> foo :DeepFrozen := {def foo implements DeepFrozen { ... }}.

By the way, I'm assuming we'll just audit everything for DeepFrozen
automatically whenever possible, or my fingers will get very tired
from typing "implements DeepFrozen" everywhere.

> How does your proposal handle the latter case? That is, in
>
>   def foo implements ... {
>     ...
>   }
>
>   def bar implements Nonsklarkish {
>     ... foo ...
>   }
>
> how does the programmer control the amount of information about foo
> which can be observed by Nonsklarkish when auditing bar?

Well, let's add the auditor first, instead of ...:

interface FooGuard guards FooAuditor {}
def foo implements FooAuditor {}
def bar implements Nonsklarkish { ... foo ... }

In both proposals, the Nonsklarkish can't see anything about foo in
this case, I think.

To make it available, I'd assume this:

  def foo :FooGuard implements FooAuditor {}

Then Nonsklarkish knows that foo was coerced by FooGuard, because "def
var :guard" exposes "guard" to auditors automatically.

Presumably for bindings the syntax would be:

  def foo as FooAuditor {}

But that gives Nonsklarkish the powerful FooAuditor, which seems
wrong, so I don't think I've understood this syntax.


-- 
Dr Thomas Leonard		ROX desktop / Zero Install
GPG: 9242 9807 C985 3C07 44A6  8B9A AE07 8280 59A5 3CC1
GPG: DA98 25AE CAD0 8975 7CDA  BD8E 0713 3F96 CA74 D8BA