[e-lang] [Caja] Functional auditor for Cajita

David-Sarah Hopwood david-sarah at jacaranda.org
Tue Dec 8 12:25:14 PST 2009


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). 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

-------------- 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/8d97ed12/attachment.bin 


More information about the e-lang mailing list