Re: [Caja] Functional auditor for Cajita [correction]

David-Sarah Hopwood wrote:
> Mark S. Miller wrote:
>> On Tue, Dec 8, 2009 at 8:47 AM,  <[email protected]> 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
>>> <[email protected]> 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

_______________________________________________
e-lang mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/e-lang

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.12 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iF4EAREIAAYFAkseukEACgkQWUc8YzyzqAddfgEAl1j9Pn/Sb0UyaQ3xB1WkoBu4
5VVbq5R8KxWsVJ8Gz/wA/iMkLVSb6jVcpm3CWfgizbwaXVwpxir7T84SxoNZAReQ
=MUwp
-----END PGP SIGNATURE-----