[e-lang] [Caja] Functional auditor for Cajita [correction]
David-Sarah Hopwood
david-sarah at jacaranda.org
Tue Dec 8 12:42:29 PST 2009
David-Sarah Hopwood wrote:
> Mark S. Miller wrote:
>> On Tue, Dec 8, 2009 at 8:47 AM, <ihab.awad at gmail.com> wrote:
>>> Thank you for the writeup; interesting. Just one point of motivation
>>> that perhaps I missed from the original post:
>>>
>>> On Mon, Dec 7, 2009 at 11:17 PM, David-Sarah Hopwood
>>> <david-sarah at jacaranda.org> wrote:
>>>> To dodge this issue, let's provisionally call a function *instance*
>>>> "copacetic" [*] if:
>>>> - that instance has only captured copacetic values, and
>>>> - it has no side effects and is deterministic whenever it is
>>>> only called with copacetic argument values, and
>>>> - it uses no side-effecting or nondeterministic primitives.
>>> I'm getting at something similar but distinct, call it "i-copacetic".
>>> :) Specifically:
>>>
>>> - it has no side effects on its lexical environment regardless
>>> of its argument values
>>>
>>> The motivation is this: An object's state is managed by some
>>> surrounding system. However, it is allowed to expose "read()" services
>>> to the outside world that do not participate in this state management.
>>> Each "read()" service may side-effect the supplied arguments, but it
>>> must not side-effect the lexical environment of the service (i.e., the
>>> object itself).
>> How is this different from E's DeepFrozen or Joe-E's Immutable?
>
> Since E has no nondeterministic ambient operations, DeepFrozen in E
> implies determinism for calls with only DeepFrozen arguments. But in
> general, if a language does have nondeterministic primitives (say,
> nondeterministic floating point arithmetic), then a copacetic function
> would be verified to be implemented in a deterministic sublanguage.
> In that case, DeepFrozen would differ from (copacetic without the
> argument and result checks).
Actually, DeepFrozen necessarily implies non-access to nondeterminism,
since otherwise a "DeepFrozen" value could be observed to change.
So DeepFrozen is the same as (copacetic without the argument and
result checks) -- or at least to what I intended that to mean, despite
some imprecision in the definition.
--
David-Sarah Hopwood ⚥ http://davidsarah.livejournal.com
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 292 bytes
Desc: OpenPGP digital signature
Url : http://www.eros-os.org/pipermail/e-lang/attachments/20091208/77139889/attachment.bin
More information about the e-lang
mailing list