Re: [Caja] Functional auditor for Cajita

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). But otherwise it is very similar.

I haven't had chance to reread the Joe-E functional purity paper yet
(http://www.cs.berkeley.edu/~daw/papers/pure-ccs08.pdf), so I'll
refrain from commenting on Immutable for the time being.

-- 
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/

iF4EAREIAAYFAksetjMACgkQWUc8YzyzqAeZzgD+Mju6zpuJs/4Yat7ucx5IPSeX
P4NMu3f0VGMra+JJ1EQA/3ndK9YV928Bz3K7WW7VaCwu7Wo9ST4OsP2UOaQ5kTd9
=TNZV
-----END PGP SIGNATURE-----